proposition: Lemma bytesToBitsK n : cancel (@bytesToBits n) (@bitsToBytes n).
proof: Proof. induction n. + move => x. by rewrite (tuple0 _) (tuple0 x). + move => xs. rewrite /bitsToBytes-/bitsToBytes/splitAtByte. rewrite (split2eta (bytesToBits xs)) split2app. case/tupleP: xs => [x xs]. rewrite /bytesToBits-/bytesToBits beheadCons theadCons. by rewrite high_catB IHn low_catB. 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