proposition: Lemma alt_Build_MeetSemiLatticeOrder : MeetSemiLatticeOrder (≤).
proof: Proof. split; try (split; try apply _). intros ?? E1 ?? E2. now rewrite !le_correct, E1, E2. split. intros ?. rewrite !le_correct. now apply (idempotency _ _). intros ? ? ?. rewrite !le_correct. intros E1 E2. now rewrite <-E1, <-associativity, E2. intros ? ?. rewrite !le_correct. intros E1 E2. now rewrite <-E2, commutativity, <-E1 at 1. intros ? ?. now rewrite le_correct, commutativity, associativity, (idempotency _ _). intros ? ?. now rewrite le_correct, <-associativity, (idempotency _ _). intros ? ? ?. rewrite !le_correct. intros E1 E2. now rewrite associativity, E1. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices