proposition: Lemma div_pow2_bits : forall a n m, (a/2^n).[m] = a.[m+n].
proof: Proof. intros a n. revert a. induct n. - intros a m. now nzsimpl. - intros n IH a m. nzsimpl; try apply le_0_l. rewrite <- div_div by order_nz. now rewrite IH, div2_bits. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog