proposition: Lemma ones_spec_high : forall n m, n<=m -> (ones n).[m] = false.
proof: Proof. intros n m ?. destruct (eq_0_gt_0_cases n) as [EQ|LT]; rewrite ones_equiv. - now rewrite EQ, pow_0_r, one_succ, pred_succ, bits_0. - apply bits_above_log2. rewrite log2_pred_pow2; trivial. rewrite <-le_succ_l, succ_pred; order. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog