omega.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.
Require Omega.

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

Local Open Scope ring_scope.
Lemma tmp:
forall p q x y, `|x - p%:Z - x| <= (max p q) /\ `|y - q%:Z - y| <= (max p q).
Proof.
    move => p q x y.
    split.
    eapply Num.Theory.ler_trans.
    Unset Printing Notations.
    have: x - p%:Z - x = -p%:Z.
    omega.