proposition: Lemma Fneg0_correct : forall x : float2, Fneg0 x = true -> (x <= 0)%R.
proof: Proof. intros (m, e) H. unfold float2R. apply F2R_le_0. simpl. revert H. unfold Fpos. simpl. now case m. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions