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