proposition: Lemma ones_add : forall n m, 0<=n -> 0<=m -> ones (m+n) == 2^m * ones n + ones m.
proof: Proof. intros n m Hn Hm. rewrite !ones_equiv. rewrite <- !sub_1_r, mul_sub_distr_l, mul_1_r, <- pow_add_r by trivial. rewrite add_sub_assoc, sub_add. reflexivity. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog