proposition: Lemma Z2int_lt x y : (Z2int x < Z2int y)%R <-> Z.lt x y.
proof: Proof. rewrite -lezD1 -[1%R]/(Z2int 1) -Z2int_add Z2int_le; lia. 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)