proposition: Lemma mul_inv_l p : /p * p = 1.
proof: Proof. destruct p as [p ?]; apply Qp.to_Qc_inj_iff; simpl. by rewrite Qcmult_inv_l, Z2Qc_inj_1 by (by apply not_symmetry, Qclt_not_eq). Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)