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