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