leP.v

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum falgebra.
From mathcomp Require Import ssrint matrix algC order.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope ring_scope.
Local Open Scope order_scope.
Import Order.Theory.

Import GRing.Theory.

Lemma tmp0: forall (x p :int), x - p - x =  -p.
move => x p.
rewrite addrAC.
rewrite subrr.
by rewrite sub0r.
Qed.

Lemma tmp:
forall (p:nat) (q:nat) (x:int) (y:int), `|x - p%:Z - x| <= (max p q) /\ `|y - q%:Z - y| <= (max p q).
Proof.
    move => p q x y.
    split.
    rewrite tmp0.
    have: forall a:nat, `|-a%:Z| = a.
    move => a.
    rewrite -[a]absz_nat.
    rewrite {1}absz_nat.
    rewrite -abszE.

    by rewrite abszN.
    move => ->.
    Fail move /leP.