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