proposition: Lemma meetK y x : join x (meet x y) = x.
proof: Proof. by apply/le_anti; rewrite join_ge_l join_le ?meet_le_l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)