proposition: Lemma min_l_iff q p : q `min` p = q ↔ q ≤ p.
proof: Proof. destruct (min_spec_le q p) as [[?->]|[?->]]; [done|]. split; [by intros ->|]. intros. by apply (anti_symm (≤)). Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)