proposition: Lemma meetA : associative meet.
proof: Proof. by move=> x y z; rewrite -{1}[x]set_meet1 -set_meetU setUA set_meetU set_meet1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)