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