proposition: Lemma double_bits_succ : forall a n, (2*a).[S n] = a.[n].
proof: Proof. intros a n. destruct (le_gt_cases 0 n) as [Hn|Hn]. - now rewrite <- div2_bits, mul_comm, div_mul by order'. - rewrite (testbit_neg_r a n Hn). apply le_succ_l in Hn. le_elim Hn. + now rewrite testbit_neg_r. + now rewrite Hn, bit0_odd, odd_mul, odd_2. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog