proposition: Theorem FtoREqInv2 : forall p q : float, p = q :>R -> Fexp p = Fexp q -> p = q.
proof: Proof. intros p q H' H'0. apply floatEq; auto. apply eq_IZR; auto. apply Rmult_eq_reg_l with (r := powerRZ radix (Fexp p)); auto with real zarith. repeat rewrite (Rmult_comm (powerRZ radix (Fexp p))); pattern (Fexp p) at 2 in |- *; rewrite H'0; auto with real zarith. now apply Rgt_not_eq, powerRZ_lt, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz