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