proposition: Lemma codeK : cancel code decode.
proof: Proof. elim=> //= v s IHs; rewrite -[_ * _]prednK ?muln_gt0 ?expn_gt0 //=. set two := 2; rewrite -[v in RHS]addn0; elim: v 0 => [|v IHv {IHs}] q. rewrite mul1n add0n /= -{}[in RHS]IHs; case: (code s) => // u; pose n := u.+1. by transitivity [rec q, n + u.+1, n.*2]; [rewrite addnn | elim: n => //=]. rewrite expnS -mulnA mul2n -{1}addnn -[_ * _]prednK ?muln_gt0 ?expn_gt0 //. set u := _.-1 in IHv *; set n := u; rewrite [in u1 in _ + u1]/n. by rewrite [in RHS]addSnnS -{}IHv; elim: n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)