JoinSemiLatticeOrder (≤). Proof. repeat split. - apply _. - apply _. - intros x. apply le_correct. apply binary_idempotent. - intros x y z E1 E2. apply le_correct in E1;apply le_correct in E2;apply le_correct. rewrite <-E2, simple_associativity, E1. reflexivity. - intros x y E1 E2. apply le_correct in E1;apply le_correct in E2. rewrite <-E1, (commutativity (f:=join)). apply symmetry;trivial. - intros. apply le_correct. rewrite simple_associativity,binary_idempotent. reflexivity. - intros;apply le_correct. rewrite (commutativity (f:=join)). rewrite <-simple_associativity. rewrite (idempotency _ _). reflexivity. - intros x y z E1 E2. apply le_correct in E1;apply le_correct in E2;apply le_correct. rewrite <-simple_associativity, E2. trivial. Qed.
Require Import