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