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