Skip to content

Instantly share code, notes, and snippets.

@vlj
Created February 16, 2020 12:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save vlj/863f47cd5a3f55f3ab545a8f1af51830 to your computer and use it in GitHub Desktop.
Save vlj/863f47cd5a3f55f3ab545a8f1af51830 to your computer and use it in GitHub Desktop.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment