proposition: Lemma bit_sub1_0 : forall i, bit (i - 1) 0 = negb (bit i 0).
proof: Proof. intro i. cut (b2i (bit (i - 1) 0) = b2i (negb (bit i 0))). generalize (bit (i - 1) 0) (negb (bit i 0)); intros b1 b2. destruct b1; destruct b2; simpl; rewrite <- eqb_spec; trivial; discriminate. replace (b2i (negb (bit i 0))) with (1 - bit i 0); [ | destruct (bit i 0); reflexivity ]. rewrite <- to_Z_eq. rewrite sub_spec, to_Z_1. rewrite 2!bit_0_spec. rewrite sub_spec, to_Z_1. case_eq (i =? 0). rewrite eqb_spec; intro Hi; rewrite Hi; reflexivity. rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0. generalize (to_Z_bounded i). intros Hi1 Hi2. rewrite (Zmod_small _ wB); [ | lia ]. assert (0 <= to_Z i mod 2 < 2)%Z. apply Z_mod_lt; lia. rewrite (Zmod_small _ wB); [ | lia ]. rewrite 2!Zmod_even. rewrite Z.even_sub. case (Z.even (to_Z i)). reflexivity. reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz