proposition: Lemma setBitThenGetSame n : forall (p: BITS n) i b, i<n -> getBit (setBit p i b) i = b.
proof: Proof. induction n => //. case/tupleP => [b' p]. move => i b LT. destruct i => //. simpl. rewrite theadCons beheadCons. assert (LT' : i < n) by done. rewrite /getBit/=. apply IHn; done. 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