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