proposition: Lemma ones_spec_low : forall n m, 0<=m<n -> (ones n).[m] = true.
proof: Proof. intros n m (Hm,H). apply testbit_true; trivial. rewrite ones_div_pow2 by (split; order). rewrite <- (pow_1_r 2). rewrite ones_mod_pow2. - rewrite ones_equiv. now nzsimpl'. - split. { order'. } apply le_add_le_sub_r. nzsimpl. now apply le_succ_l. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog