proposition: Theorem rdiv3b a b c d e : ~ (b * e) == 0 -> ~ (d * e) == 0 -> a / (b*e) - c / (d*e) == (a * d - c * b) / (b * (d * e)).
proof: Proof. intros H H0. rewrite !rsub_def, rdiv5, ropp_mul_l. now apply rdiv2b. Qed.
imports: ZArith_base