proposition: Theorem Dekker1: (radix=2)%Z \/ (Nat.Even t) -> (x*y=r-t4)%R.
proof: Proof. case Cy; case Cx; intros. unfold FtoRradix; apply DekkerN with b t p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 t1 t2 t3; auto. unfold FtoRradix; apply DekkerS2 with b t p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 t1 t2 t3; auto. unfold FtoRradix; apply DekkerS1 with b t p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 t1 t2 t3; auto. absurd (- dExp b <= Fexp x + Fexp y)%Z; auto with zarith. apply Zlt_not_le. elim H; intros T1 T2; elim T2; intros G1 T; clear T1 T2 T. elim H0; intros T1 T2; elim T2; intros G2 T; clear T1 T2 T. rewrite G1; rewrite G2; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz