proposition: Lemma n_compC a e : n_comp e T = n_comp e a + n_comp e [predC a].
proof: Proof. rewrite /n_comp_mem (eq_card (fun _ => andbT _)) -(cardID a); congr (_ + _). by apply: eq_card => x; rewrite !inE andbC. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)