proposition: Lemma seq_block_inv A : forall r (l : seq A) k, size l = r * k.+1 -> exists l1 l2, l = l1 ++ l2 /\ size l1 = r /\ size l2 = r * k.
proof: Proof. elim=> [l r | r IH l [ | k H] ]. - rewrite !mul0n => Hl. by exists l, nil; rewrite cats0. - rewrite muln1 => H. exists (take (r.+1) l), nil. by rewrite cats0 take_oversize; [rewrite muln0 | rewrite H]. - exists (take (r.+1) l), (drop (r.+1) l). rewrite cat_take_drop size_drop H size_take H ltn_Pmulr //. repeat (split => //). by rewrite -{2}(muln1 (r.+1)) -(mulnBr (r.+1)). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code