proposition: Lemma land_ones_low : forall a n, log2 a < n -> land a (ones n) == a.
proof: Proof. intros; rewrite land_ones. apply mod_small. apply log2_lt_cancel. rewrite log2_pow2; trivial using le_0_l. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog