proposition: Lemma toF_zero : toF zero = Fzero.
proof: Proof. unfold toF; simpl. generalize (mantissa_sign_correct mantissa_zero). rewrite mantissa_zero_correct. now destruct mantissa_sign; try easy; destruct s; intros []; discriminate. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig