proposition: Lemma ones_div_pow2 : forall n m, m<=n -> ones n / 2^m == ones (n-m).
proof: Proof. intros n m H. symmetry. apply div_unique with (ones m). - rewrite ones_equiv. apply le_succ_l. rewrite succ_pred; order_nz. - rewrite <- (sub_add m n H) at 1. rewrite (add_comm _ m). apply ones_add. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog