proposition: Lemma div2_bits : forall a n, 0<=n -> (a/2).[n] = a.[S n].
proof: Proof. intros a n Hn. apply eq_true_iff_eq. rewrite 2 testbit_true by order_pos. rewrite pow_succ_r by trivial. now rewrite div_div by order_pos. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog