proposition: Lemma meets_seq I (r : seq I) (F : I -> L) : \meet_(i <- r) F i = \meet_(i in r) F i.
proof: Proof. by rewrite -big_enum; apply/eq_big_idem => ?; rewrite /= ?meetxx ?mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)