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