proposition: Lemma bits_opp : forall a n, 0<=n -> (-a).[n] = negb (P a).[n].
proof: Proof. intros a n Hn. destruct (testbit_spec (-a) n Hn) as (l & h & Hl & EQ). fold (b2z (-a).[n]) in EQ. apply negb_sym. apply testbit_unique with (2^n-l-1) (-h-1). - split. + apply lt_succ_r. rewrite sub_1_r, succ_pred. now apply lt_0_sub. + apply le_succ_l. rewrite sub_1_r, succ_pred. apply le_sub_le_add_r. rewrite <- (add_0_r (2^n)) at 1. now apply add_le_mono_l. - rewrite <- add_sub_swap, sub_1_r. f_equiv. apply opp_inj. rewrite opp_add_distr, opp_sub_distr. rewrite (add_comm _ l), <- add_assoc. rewrite EQ at 1. apply add_cancel_l. rewrite <- opp_add_distr. rewrite <- (mul_1_l (2^n)) at 2. rewrite <- mul_add_distr_r. rewrite <- mul_opp_l. f_equiv. rewrite !opp_add_distr. rewrite <- mul_opp_r. rewrite opp_sub_distr, opp_involutive. rewrite (add_comm h). rewrite mul_add_distr_l. rewrite !add_assoc. apply add_cancel_r. rewrite mul_1_r. rewrite add_comm, add_assoc, !add_opp_r, sub_1_r, two_succ, pred_succ. destruct (-a).[n]; simpl. + now rewrite sub_0_r. + now nzsimpl'. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog