proposition: Lemma ones_spec_high : forall n m, 0<=n<=m -> (ones n).[m] = false.
proof: Proof. intros n m (Hn,H). le_elim Hn. - apply bits_above_log2; rewrite ones_equiv. + rewrite <-lt_succ_r, succ_pred; order_pos. + rewrite log2_pred_pow2; trivial. now rewrite <-le_succ_l, succ_pred. - rewrite ones_equiv. now rewrite <- Hn, pow_0_r, one_succ, pred_succ, bits_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog