proposition: Lemma bitsEq_decomp n b1 b2 (p1 p2: BITS n) : (consB b1 p1 == consB b2 p2) = (b1 == b2) && (p1 == p2).
proof: Proof. done. 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