proposition: Lemma subB_eq0 n (x y: BITS n) : (subB x y == #0) = (x == y).
proof: Proof. destruct n. by rewrite (tuple0 x) (tuple0 y). rewrite 2!toZp_eq. autorewrite with ZpHom. by rewrite subr_eq0. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)