proposition: Theorem addf_3 : 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