proposition: Lemma toF_float : forall s p e, valid_mantissa p -> toF (float_aux s p e) = Basic.Float s (MtoP p) (EtoZ e).
proof: Proof. intros. simpl. generalize (mantissa_sign_correct ((if s then mantissa_neg else mantissa_pos) p)). case (mantissa_sign ((if s then mantissa_neg else mantissa_pos) p)). case s. rewrite mantissa_neg_correct. intro H0 ; discriminate H0. exact H. rewrite mantissa_pos_correct. intro H0 ; discriminate H0. exact H. intros t q. case s. rewrite mantissa_neg_correct. case t ; intros (H1, H2). now inversion H1. discriminate H1. exact H. rewrite mantissa_pos_correct. case t ; intros (H1, H2). discriminate H1. now inversion H1. exact H. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig