proposition: Lemma Z2int_le x y : (Z2int x <= Z2int y)%R <-> Z.le x y.
proof: Proof. rewrite /Z2int; case Ex: x; case Ey: y=> //. { rewrite oppr_ge0; split; move=> H; exfalso; move: H; [|by rewrite /Z.le]. apply/negP; rewrite -ltNge; apply nat_of_pos_gt0. } { split; move=> H; exfalso; move: H; [|by rewrite /Z.le]. apply/negP; rewrite -ltNge; apply nat_of_pos_gt0. } { rewrite -!binnat.to_natE /Num.Def.ler /=. by rewrite -!positive_nat_Z -Nat2Z.inj_le; split => /ssrnat.leP. } { split; move=> H; exfalso; move: H; [|by rewrite /Z.le]. apply /negP; rewrite -ltNge. by apply: (@lt_trans _ _ 0%R); rewrite ?oppr_lt0; apply nat_of_pos_gt0. } { rewrite oppr_le0; split; by rewrite /Z.le. } { split=>_; [by rewrite /Z.le|]. by apply: (@le_trans _ _ 0%R); [apply oppr_le0|apply ltW, nat_of_pos_gt0]. } rewrite lerN2; split. { rewrite /Z.le /Z.compare -!binnat.to_natE /Num.Def.ler /= => /ssrnat.leP. by rewrite -Pos.compare_antisym -Pos2Nat.inj_le -Pos.compare_le_iff. } rewrite /Z.le /Z.compare -!binnat.to_natE /Num.Def.ler /=. rewrite -Pos.compare_antisym => H; apply/ssrnat.leP. by rewrite -Pos2Nat.inj_le -Pos.compare_le_iff. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)