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