proposition: Lemma mantissa_sign_correct : forall x, match mantissa_sign x with | Mzero => MtoZ x = Z0 | Mnumber s p => MtoZ x = (if s then Zneg else Zpos) (MtoP p) /\ valid_mantissa p end.
proof: Proof. intros. case x ; repeat split. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig