proposition: Lemma min_spec q p : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
proof: Proof. unfold min. destruct (decide (q ≤ p)) as [[?| ->]%le_lteq|?]; [by auto..|]. right. split; [|done]. by apply lt_le_incl, lt_nge. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)