proposition: Lemma pos_to_Qp_mul x y : pos_to_Qp x * pos_to_Qp y = pos_to_Qp (x * y).
proof: Proof. apply Qp.to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)