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. unfold mantissa_sign. rewrite BigZ.spec_eqb. case Z.eqb_spec. easy. change (BigZ.to_Z 0%bigZ) with Z0. case x ; unfold valid_mantissa ; simpl ; intros ; rename n into H. assert (BigN.to_Z t = Zpos (MtoP t)). generalize H. clear. unfold MtoP. generalize (BigN.spec_pos t). case (BigN.to_Z t) ; intros. elim H0. apply refl_equal. apply refl_equal. elim H. apply refl_equal. split. exact H0. exists (MtoP t). exact H0. assert (- BigN.to_Z t = Zneg (MtoP t))%Z. generalize H. clear. unfold MtoP. generalize (BigN.spec_pos t). case (BigN.to_Z t) ; intros. elim H0. apply refl_equal. apply refl_equal. elim H. apply refl_equal. split. exact H0. exists (MtoP t). exact (BinInt.Z.opp_inj _ (Zpos _) H0). Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig