proposition: Theorem rdiv7 a b c d : ~ b == 0 -> ~ c == 0 -> ~ d == 0 -> (a / b) / (c / d) == (a * d) / (b * c).
proof: Proof. intros. rewrite (rdiv_def (a / b)). rewrite rdiv6; trivial. apply rdiv4; trivial. Qed.
imports: ZArith_base