proposition: Lemma even_ctrace et : even_trace (ctrace et) = even_trace et.
proof: Proof. case: et => // e et; rewrite /ctrace /even_trace /ttail /proper_trace /=. case: ifP => //= _; move Dg: (edge_rot e) => g. have{Dg}: cbit1 (g e) = false by rewrite -Dg; case e. elim: et e => [|e' et IHet] e /= ge1; first by rewrite addc0; case: (g e) ge1. by case Dge': (g e'); rewrite //= addcA IHet // permc_addc cbit1_addc ge1 Dge'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)