proposition: Lemma inv_mul_distr p q : /(p * q) = /p * /q.
proof: Proof. apply (inj (mul (p * q))). rewrite mul_inv_r, (comm_L mul p), <-(assoc_L _), (assoc_L mul p). by rewrite mul_inv_r, mul_1_l, mul_inv_r. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)