proposition: Lemma toNat_decB_succ n : forall (p: BITS n), (toNat (decB p)).+1 = if p == #0 then 2^n else toNat p.
proof: Proof. induction n. + move => p. by rewrite (tuple0 p). + case/tupleP => [b p]. rewrite /=theadCons beheadCons toNatCons. destruct b => //. rewrite toNat_joinlsb add0n. specialize (IHn p). case E: (p == #0) => //. + rewrite (eqP E). rewrite (eqP E) eq_refl in IHn. rewrite expnS. rewrite -IHn. replace (_ == _) with true. by rewrite add1n mul2n doubleS. rewrite /fromNat-/fromNat/=/joinlsb. simpl. by rewrite eq_refl. + replace (_ == _) with false. rewrite E in IHn. rewrite -IHn. rewrite doubleS. by rewrite add1n. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations