proposition: Theorem Dekker_FTS : forall p q : float, Fbounded b p -> Fbounded b q -> (Rabs q <= Rabs p)%R -> Iminus q (Iminus (Iplus p q) p) = (p + q - Iplus p q)%R :>R.
proof: Proof. intros p q H' H'0 H'1. apply MDekkerAux1; auto. apply MDekker; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz