proposition: Lemma negB_or_invB_fromNat n : forall m, m < 2^n -> negB (n:=n) #m = #(2^n - m) /\ invB (n:=n) #m = #((2^n).-1 - m).
proof: Proof. induction n. split; [done | apply trivialBits]. move => m H. rewrite expnS mul2n in H. pose H' := half_ltn_double H. elim (IHn _ H') => [IH1 IH2] {IHn}. split. + rewrite /negB. rewrite /fromNat-/fromNat. rewrite invBCons IH2 /=!theadCons!beheadCons. rewrite oddB. rewrite odd_power2/=. case ODD: (odd m). - rewrite expnS mul2n. rewrite half_sub. rewrite uphalf_half ODD -subn1 subnDA. done. apply (ltnW H). - rewrite incB_fromNat. rewrite expnS mul2n half_sub. rewrite uphalf_half ODD add0n. rewrite -subn1. rewrite subnAC. rewrite subn1. rewrite prednK. done. by rewrite subn_gt0. apply (ltnW H). - rewrite expnS mul2n. apply (ltnW H). rewrite /fromNat-/fromNat invBCons IH2. rewrite oddB/=. rewrite odd_power2subn1/=. rewrite -!subn1 -!subnDA expnS mul2n. rewrite half_sub. done. apply H. rewrite expnS mul2n. apply leq_subn; last done. rewrite -mul2n -expnS. apply expn_gt0. 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)