proposition: Lemma joinEseq s1 s2 : s1 `|` s2 = match s1, s2 with | [::], _ => s2 | _, [::] => s1 | x1 :: s1', x2 :: s2' => (x1 `|` x2) :: ((s1' : seq _) `|` s2') end.
proof: Proof. by case: s1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)