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