proposition: Lemma Zcompare_correct: forall x y, match x ?= y with Eq => x = y | Gt => x > y | Lt => x < y end.
proof: Proof. intros x y; unfold Z.lt, Z.gt; generalize (Zcompare_Eq_eq x y); case Z.compare; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod