proposition: Lemma allBitsEq n (p q: BITS n) : (forall i, i < n -> getBit p i = getBit q i) -> p = q.
proof: Proof. induction n. by rewrite (tuple0 p) (tuple0 q). case/tupleP: p => [b p]. case/tupleP: q => [c q]. move => H. have H0:= H 0. rewrite /getBit/= in H0. rewrite H0 => //. rewrite (IHn p q). done. move => i LT. apply (H i.+1 LT). 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