proposition: Lemma joinlsbK n : cancel (@joinlsb n) (@splitlsb n).
proof: Proof. move => [p b]. by rewrite /joinlsb /splitlsb beheadCons theadCons. 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