proposition: Lemma min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
proof: Proof. destruct (min_spec q p) as [[?%lt_le_incl ?]|]; [left|right]; done. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)