proposition: Theorem floatEq : forall p q : float, Fnum p = Fnum q -> Fexp p = Fexp q -> p = q.
proof: Proof. intros p q; case p; case q; simpl in |- *; intros; apply (f_equal2 (A1:=Z) (A2:=Z)); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz