proposition: Lemma exponent_cmp_correct : forall x y, exponent_cmp x y = Z.compare (MtoZ x) (MtoZ y).
proof: Proof. intros. unfold exponent_cmp, MtoZ. apply sym_eq. generalize (BigZ.spec_compare x y). unfold Z.lt, Z.gt. case (x ?= y)%bigZ ; intro H ; rewrite H ; first [ apply Z.compare_refl | apply refl_equal ]. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig