proposition: Lemma decodeK : cancel decode code.
proof: Proof. have m2s: forall n, n.*2 - n = n by move=> n; rewrite -addnn addnK. case=> //= n; rewrite -[n.+1]mul1n -(expn0 2) -[n in RHS]m2s. elim: n {2 4}n {1 3}0 => [|q IHq] [|[|r]] v //=; rewrite {}IHq ?mul1n ?m2s //. by rewrite expnSr -mulnA mul2n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)