proposition: Lemma div2_bits : forall a n, (a/2).[n] = a.[S n].
proof: Proof. intros. apply eq_true_iff_eq. rewrite 2 testbit_true. rewrite pow_succ_r by apply le_0_l. now rewrite div_div by order_nz. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog