proposition: Lemma enum0 : enum 'I_0 = [::].
proof: Proof. by apply/nilP; rewrite /nilp size_enum_ord. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)