proposition: Lemma set1_disjoint (T : finType) (i j : T) : [set i] != [set j] -> [disjoint [set i] & [set j]].
proof: Proof. move=> Hneq; rewrite /disjoint; apply/pred0P => l /=; apply: negbTE. by rewrite !in_set1; move: Hneq; apply: contra => /andP[/eqP-> /eqP->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)