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