proposition: Theorem sameExpEq : forall p q : float, p = q :>R -> Fexp p = Fexp q -> p = q.
proof: Proof. intros p q; case p; case q; unfold FtoR in |- *; simpl in |- *. intros Fnum1 Fexp1 Fnum2 Fexp2 H' H'0; rewrite H'0; rewrite H'0 in H'. cut (Fnum1 = Fnum2). intros H'1; rewrite <- H'1; auto. apply eq_IZR; auto. apply Rmult_eq_reg_l with (r := powerRZ radix Fexp1); repeat rewrite (Rmult_comm (powerRZ radix Fexp1)); auto. apply Rlt_dichotomy_converse; right; auto with real. red in |- *; auto with real. now apply powerRZ_lt, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz