proposition: Lemma mantissa_even_correct : forall x, valid_mantissa x -> mantissa_even x = Z.even (Zpos (MtoP x)).
proof: Proof. intros x (px, Hx). unfold mantissa_even, Zeven, MtoP. generalize (BigN.spec_even x). rewrite Hx. case (BigN.even x) ; destruct px as [px|px|] ; try easy. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig