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