proposition: Lemma urtrace_trace (lc : colseq) : urtrace (rot 1 lc) = trace lc.
proof: Proof. case: lc => [|c1 [|c2 lc]]; rewrite /urtrace /rot //= ?addcc // last_cat /=. rewrite /ctrace /= cats1 -addcA; congr (_ :: _). elim: lc c2 => [|c3 lc IHlc] c2 /=; first by rewrite addc0 addcC. by rewrite -addcA addKc -IHlc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)