proposition: Lemma Qmin_coincides x y : Qmin x y = x ⊓ y.
proof: Proof. destruct (total (≤) x y). rewrite lattices.meet_l by easy. now apply Qle_min_l. rewrite lattices.meet_r by easy. now apply Qle_min_r. Qed.
imports: CoRN.model.totalorder.QMinMax MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.orders.minmax MathClasses.implementations.stdlib_rationals