proposition: Lemma ones_mod_pow2 : forall n m, 0<=m<=n -> (ones n) mod (2^m) == ones m.
proof: Proof. intros n m (Hm,H). symmetry. apply mod_unique with (ones (n-m)). - left. rewrite ones_equiv. split. + rewrite <- lt_succ_r, succ_pred. order_pos. + now rewrite <- le_succ_l, succ_pred. - rewrite <- (sub_add m n) at 1. rewrite (add_comm _ m). apply ones_add; trivial. now apply le_0_sub. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog