proposition: Lemma land_ones : forall a n, land a (ones n) == a mod 2^n.
proof: Proof. intros a n. bitwise as m. destruct (le_gt_cases n m). - now rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r. - now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog