proposition: Lemma bound_meetKU b2 b1 : bound_join b1 (bound_meet b1 b2) = b1.
proof: Proof. case: b1 b2 => [? ?|[]][? ?|[]] //=; rewrite ?meetKU ?joinxx ?leIl ?lexI ?lexx ?andbb //=; congr BSide. by case: lcomparableP; rewrite ?orbF /= ?andbb ?orbK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)