proposition: Lemma to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q.
proof: Proof. split; [|by intros ->]. destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _). Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)