proposition: Lemma lowBitsEq n1 n2 (p q: BITS (n1+n2)) : (forall i, i < n1 -> getBit p i = getBit q i) <-> low n1 p = low n1 q.
proof: Proof. induction n1 => //=. case/tupleP: p => [b p]. fold plus in p. case/tupleP: q => [c q]. fold plus in q. rewrite 2!beheadCons 2!theadCons /getBit/=. split => H. + have H0:= H 0. rewrite /= in H0. rewrite H0 => //. rewrite (proj1 (IHn1 p q)). done. move => i LT. apply (H i.+1 LT). + move => i LT. destruct i. by injection H. injection H => H1 H2. subst. apply (IHn1 p q). apply val_inj. apply H1. apply 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