le_refl.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.
From mathcomp Require Import ssrint matrix order ssrint order.


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

Local Open Scope ring_scope.
Import Order.Theory.

Import GRing.Theory.
Import Num.Theory.

Lemma tmp0: forall (x p :int), x - p - x = -p.
Unset Printing Notations.


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| <= (Num.max p%:Z q)%R /\ `|y - q%:Z - y| <= (Num.max p%:Z 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 => ->.
    rewrite ler_maxr.
    Unset Printing Notations.
    rewrite (le_refl p).