proposition: Lemma etail_perm et : proper_trace et -> {g | permt g et = Color1 :: etail et}.
proof: Proof. rewrite -ttail_etrace /ttail /etrace; move: (etrace_perm et) => h. rewrite -(proper_permt h) => et_ok; rewrite et_ok. case Dhet: (permt h et) => //= [e het'] in et_ok *. have [g Dget] := (compose_permt (edge_rot e) h et); exists g. by rewrite {}Dget {}Dhet; case: e in et_ok *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)