proposition: Lemma div_mul_cancel_l p q r : (r * p) / (r * q) = p / q.
proof: Proof. rewrite <-div_div. f_equiv. unfold div. by rewrite (comm_L mul r), <-(assoc_L _), mul_inv_r, mul_1_r. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)