proposition: Lemma land_ones_low : forall a n, 0<=a -> log2 a < n -> land a (ones n) == a.
proof: Proof. intros a n Ha H. assert (Hn : 0<=n) by (generalize (log2_nonneg a); order). rewrite land_ones; trivial. apply mod_small. split; trivial. apply log2_lt_cancel. now rewrite log2_pow2. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog