proposition: Theorem LeFnumZERO : forall x : float, (0 <= Fnum x)%Z -> (0 <= x)%R.
proof: Proof. intros x H'; unfold FtoRradix, FtoR in |- *. replace 0%R with (0%Z * 0%Z)%R; auto 6 with real zarith. apply Rmult_le_compat; try apply IZR_le; auto with real zarith. now apply powerRZ_le, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz