proposition: Lemma ones_mod_pow2 : forall n m, m<=n -> (ones n) mod (2^m) == ones m.
proof: Proof. intros n m H. symmetry. apply mod_unique with (ones (n-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