proposition: Lemma Flt2_m1_correct : forall f, Flt2_m1 f = true -> (-1 < f)%R.
proof: Proof. intros f Hb. generalize (Flt2_correct _ _ Hb). unfold float2R, F2R. simpl. now rewrite Rmult_1_r. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions