proposition: Lemma meetEseq s1 s2 : s1 `&` s2 = [seq x.1 `&` x.2 | x <- zip s1 s2].
proof: Proof. by elim: s1 s2 => [|x s1 ihs1] [|y s2]//=; rewrite -ihs1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)