proposition: Lemma urtrace_rot (lc : colseq) : urtrace (rot 1 lc) = rot 1 (urtrace lc).
proof: Proof. case: lc => [|c1 [|c2 lc]]; rewrite /urtrace /rot //= last_cat /= !cats1. by congr (_ :: _); elim: lc c2 => //= c3 lc IHlc c2; rewrite IHlc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)