proposition: Lemma memc0_permt g et : (Color0 \in permt g et) = (Color0 \in et).
proof: Proof. by elim: et => [|e et IHet] //=; rewrite !inE IHet !(eq_sym Color0) permc_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)