proposition: Theorem LtFnumZERO : forall x : float, (0 < Fnum x)%Z -> (0 < x)%R.
proof: Proof. intros x; case x; unfold FtoR in |- *; simpl in |- *. intros Fnum1 Fexp1 H'; replace 0%R with (Fnum1 * 0)%R; [ apply Rmult_lt_compat_l | ring ]; auto with real zarith. now apply IZR_lt. now apply powerRZ_lt, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz