proposition: Lemma ptrace_addc c (lc : colseq) : ptrace (map (addc c) lc) = ptrace lc.
proof: Proof. rewrite /ptrace; case: lc => //= c' lc; elim: lc c' => //= c'' lc IHlc c'. by rewrite (addcC c) -addcA addKc IHlc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)