proposition: Theorem cross_product_eq a b c d : ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d.
proof: Proof. intros H H0 H1. transitivity (a / b * (d / d)). - now rewrite rdiv_r_r, rmul_1_r. - now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r. Qed.
imports: ZArith_base