MeetSemiLatticeOrder (≤). Proof. repeat split. - apply _. - apply _. - intros ?. apply le_correct. apply (idempotency _ _). - intros ? ? ? E1 E2. apply le_correct in E1;apply le_correct in E2;apply le_correct. rewrite <-E1, <-simple_associativity, E2. reflexivity. - intros ? ? E1 E2. apply le_correct in E1;apply le_correct in E2. rewrite <-E2, (commutativity (f:=meet)). apply symmetry,E1. - intros ? ?. apply le_correct. rewrite (commutativity (f:=meet)), simple_associativity, (idempotency _ _). reflexivity. - intros ? ?. apply le_correct. rewrite <-simple_associativity, (idempotency _ _). reflexivity. - intros ? ? ? E1 E2. apply le_correct in E1;apply le_correct in E2;apply le_correct. rewrite associativity, E1. trivial. Qed.
Require Import