proposition: Lemma trace_rev (lc : colseq) : trace (rev lc) = rot 1 (rev (trace lc)).
proof: Proof. case: lc => // c0 lc; rewrite -!urtrace_trace !urtrace_rot; congr (rot 1 _). elim/last_ind: lc => // lc c /(congr1 behead). case/lastP: lc => [|lc c']; first by rewrite /urtrace /= (addcC c). rewrite -!rcons_cons !rev_rcons -2!rot1_cons !urtrace_rot -urtrace_rot. do 2!rewrite /urtrace /= ?rot1_cons /=; rewrite !rev_rcons /= => <-. by rewrite rev_cons cats1 !last_rcons !(addcC c). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)