proposition: Theorem Rlt_Fexp_eq_Zlt : 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 lt_IZR. apply (Rlt_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