proposition: Lemma bitsToBytesK n : cancel (@bitsToBytes n) (@bytesToBits n).
proof: Proof. induction n. + move => x. by rewrite (tuple0 _) (tuple0 x). + move => xs. rewrite /bitsToBytes-/bitsToBytes. rewrite /splitAtByte. rewrite (split2eta xs) split2app. by rewrite /bytesToBits-/bytesToBits beheadCons theadCons IHn. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec