proposition: Theorem LtR0Fnum : forall p : float, (0 < p)%R -> (0 < Fnum p)%Z.
proof: Proof. intros p H'. apply lt_IZR. apply (Rlt_monotony_contra_exp radix) with (z := Fexp p); auto with real arith. simpl in |- *; rewrite Rmult_0_l; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz