proposition: Theorem Rle_Fexp_eq_Zle : forall x y : float, (x <= y)%R -> Fexp x = Fexp y -> (Fnum x <= Fnum y)%Z.
proof: Proof. intros x y H' H'0. apply le_IZR. apply (Rle_monotony_contra_exp radix) with (z := Fexp x); auto with real arith. pattern (Fexp x) at 2 in |- *; rewrite H'0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz