proposition: Lemma Rsgn_F2R : forall m e, Rlt_bool (F2R (Float beta m e)) 0 = Zlt_bool m 0.
proof: Proof. intros m e. case Zlt_bool_spec ; intros H. apply Rlt_bool_true. now apply F2R_lt_0. apply Rlt_bool_false. now apply F2R_ge_0. Qed.
imports: Coq(ZArith Reals) Flocq(Core Bracket Round Operations Div Sqrt)