proposition: Lemma bound_meetA : associative bound_meet.
proof: Proof. case=> [? x|[]][? y|[]][? z|[]] //=; rewrite !lexI meetA; congr BSide. by case: (lcomparableP x y) => [|||->]; case: (lcomparableP y z) => [|||->]; case: (lcomparableP x z) => [|||//<-]; case: (lcomparableP x y); rewrite //= ?andbF ?orbF ?lexx ?orbA //; case: (lcomparableP y z). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)