proposition: Lemma highBitsEq n1 n2 (p q: BITS (n1+n2)) : (forall i, n1 <= i -> getBit p i = getBit q i) <-> high n2 p = high n2 q.
proof: Proof. induction n1 => /=. split. have ABE := @allBitsEq _ p q. move => H. apply: ABE. move => i H'. rewrite H => //. by move => ->. case/tupleP: p => [b p]. fold plus in p. case/tupleP: q => [c q]. fold plus in q. rewrite 2!beheadCons /getBit/=. split => H. + apply IHn1. move => i LE. apply (H i.+1 LE). + have IH' := (proj2 (IHn1 p q)). case => // i. by apply IH'. 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