proposition: Lemma ones_equiv : forall n, ones n == P (2^n).
proof: Proof. intros n. unfold ones. destruct (le_gt_cases 0 n). - now rewrite shiftl_mul_pow2, mul_1_l. - f_equiv. rewrite pow_neg_r; trivial. rewrite <- shiftr_opp_r. apply shiftr_eq_0_iff. right; split. { order'. } rewrite log2_1. now apply opp_pos_neg. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog