proposition: Lemma land_ones : forall a n, 0<=n -> land a (ones n) == a mod 2^n.
proof: Proof. intros a n Hn. bitwise as m ?. destruct (le_gt_cases n m). - rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r; try split; trivial. - rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r; try split; trivial. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog