proposition: Lemma lnot_land_low : forall a b n, log2 a < n -> log2 b < n -> lnot (land a b) n == lor (lnot a n) (lnot b n).
proof: Proof. intros a b n Ha Hb. bitwise as m. destruct (le_gt_cases n m). - rewrite !lnot_spec_high, land_spec, !bits_above_log2; trivial. + now apply lt_le_trans with n. + now apply lt_le_trans with n. - now rewrite !lnot_spec_low, land_spec, negb_andb. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog