fact: Fixpoint meet s1 s2 := match s1, s2 with | x1 :: s1', x2 :: s2' => (x1 `&` x2) :: meet s1' s2' | _, _ => [::] end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)