proposition: Theorem floatDec : forall x y : float, {x = y} + {x <> y}.
proof: Proof. intros x y; case x; case y; intros Fnum2 Fexp2 Fnum1 Fexp1. case (Z.eq_dec Fnum1 Fnum2); intros H1. case (Z.eq_dec Fexp1 Fexp2); intros H2. left; apply floatEq; auto. right; red in |- *; intros H'; contradict H2; inversion H'; auto. right; red in |- *; intros H'; contradict H1; inversion H'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz