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