proposition: Lemma other_colors c : c != Color0 -> pred4 Color0 c (Eperm312 c) (Eperm231 c) =i color.
proof: Proof. by case: c => // _ []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)