proposition: Lemma color_inj_permc f : injective f -> f Color0 = Color0 -> {g : edge_perm | f =1 g}.
proof: Proof. move/inj_eq=> injf f0; have Ef0 := injf Color0; rewrite f0 in Ef0. case f1: (f Color1) (Ef0 Color1) (injf Color1) => // _ Ef1; case f2: (f Color2) (Ef0 Color2) (Ef1 Color2) {injf}(injf Color2) => // _ _ Ef2; [ exists Eperm123 | exists Eperm132 | exists Eperm213 | exists Eperm231 | exists Eperm312 | exists Eperm321] => [] [] //; by case: (f Color3) (Ef0 Color3) (Ef1 Color3) (Ef2 Color3). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)