proposition: Fact ex1 : forall (f : float r), (0 <= Fnum f)%Z <-> 0 <= F2R f.
proof: Proof. intros [mf ef]; unfold F2R; simpl; split; intro HH. - apply Rmult_le_pos. apply (IZR_le 0); auto. apply bpow_ge_0. - apply le_IZR; simpl. apply (Rmult_le_reg_r (bpow r ef)). apply bpow_gt_0. lra. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)