proposition: Lemma lt_ge_cases p q : {p < q} + {q ≤ p}.
proof: Proof. refine (cast_if (Qclt_le_dec (Qp_to_Qc p) (Qp_to_Qc q)%Qc)); [by apply to_Qc_inj_lt|by apply to_Qc_inj_le]. Defined.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)