proposition: Lemma bound_leEmeet b1 b2 : (b1 <= b2) = (bound_meet b1 b2 == b1).
proof: Proof. case: b1 b2 => [[]t[][]|[][][]] //=; rewrite ?eqxx// => t'; rewrite [LHS]/<=%O /eq_op ?andbT ?andbF ?orbF/= /eq_op/= /eq_op/=; case: lcomparableP => //=; rewrite ?eqxx//=; [| | |]. - by move/lt_eqF. - move=> ic; apply: esym; apply: contraNF ic. by move=> /eqP/meet_idPl; apply: le_comparable. - by move/lt_eqF. - move=> ic; apply: esym; apply: contraNF ic. by move=> /eqP/meet_idPl; apply: le_comparable. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)