proposition: Theorem R0LeFnum : forall p : float, (p <= 0)%R -> (Fnum p <= 0)%Z.
proof: Proof. intros p H'. apply le_IZR. apply (Rle_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