proposition: Theorem addf_2 : forall a b : R, forall zi : FF, NZR (a + b) -> BND (1 - b / (a + b)) zi -> BND (a / (a + b)) zi.
proof: Proof. intros a b zi Hab Hz. replace (a / (a + b))%R with (1 - b / (a + b))%R. exact Hz. field. exact Hab. Qed.
imports: Reals Gappa_common