proposition: Lemma toNat_negB_or_invB n : forall (p: BITS n), (toNat (negB p) = if toNat p == 0 then 0 else 2^n - toNat p) /\ (toNat (invB p) = (2^n).-1 - toNat p).
proof: Proof. induction n. move => p. by rewrite (tuple0 p)/toNat/=. case/tupleP => [b p]. rewrite /negB !invBCons!toNatCons/=!theadCons!beheadCons. elim (IHn p) => [IH1 IH2]. split. case b. + simpl. rewrite toNatCons IH2. rewrite doubleB expnS mul2n. rewrite -subn1 doubleB/=. rewrite add1n. rewrite -!mul2n. rewrite muln1. rewrite subnAC. rewrite subn2. rewrite subnDA. rewrite subnAC. rewrite prednK. by rewrite subn1. assert (B:=toNatBounded p). rewrite !mul2n -doubleB. rewrite -subn1. rewrite subn_gt0. rewrite -subn_gt0 in B. rewrite -half_gt0. rewrite doubleK. done. + simpl. rewrite toNatCons. rewrite !add0n. rewrite /negB in IH1. rewrite IH1. case E: (toNat p) => [| n']. done. simpl. rewrite doubleB expnS -muln2 mulnC. done. case b. + simpl. rewrite add0n. rewrite IH2. rewrite expnS. rewrite -!subn1 !doubleB. rewrite -!muln2. rewrite mul1n subnDA. rewrite mulnC. rewrite !subn1 subn2. done. + simpl. rewrite add0n. rewrite IH2. rewrite expnS. rewrite -!subn1 !doubleB. rewrite -!muln2. rewrite mul1n. rewrite add1n. rewrite subnAC. rewrite mulnC. rewrite subn2. assert (B:0 < (2*2^n - toNat p * 2).-1). assert (B':=toNatBounded p). rewrite mul2n muln2. rewrite -doubleB. rewrite -subn_gt0 in B'. rewrite -subn1 subn_gt0 -half_gt0 doubleK. done. rewrite (ltn_predK B). rewrite -subn1. by rewrite subnAC. 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 mathcomp(ssralg)