proposition: Lemma Qmax_coincides x y : Qmax x y = x ⊔ y.
proof: Proof. destruct (total (≤) x y). rewrite lattices.join_r by easy. now apply Qle_max_r. rewrite lattices.join_l by easy. now apply Qle_max_l. Qed.
imports: CoRN.model.totalorder.QMinMax MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.orders.minmax MathClasses.implementations.stdlib_rationals