proposition: Lemma ones_add : forall n m, ones (m+n) == 2^m * ones n + ones m.
proof: Proof. intros n m. rewrite !ones_equiv. rewrite <- !sub_1_r, mul_sub_distr_l, mul_1_r, <- pow_add_r. rewrite add_sub_assoc, sub_add. - reflexivity. - apply pow_le_mono_r. { order'. } rewrite <- (add_0_r m) at 1. apply add_le_mono_l, le_0_l. - rewrite <- (pow_0_r 2). apply pow_le_mono_r. { order'. } apply le_0_l. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog