proposition: Lemma ones_spec_low : forall n m, m<n -> (ones n).[m] = true.
proof: Proof. intros. apply testbit_true. rewrite ones_div_pow2 by order. rewrite <- (pow_1_r 2). rewrite ones_mod_pow2. - rewrite ones_equiv. now nzsimpl'. - apply le_add_le_sub_r. nzsimpl. now apply le_succ_l. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog