proposition: Lemma lnot_lxor_r : forall a b n, lnot (lxor a b) n == lxor a (lnot b n).
proof: Proof. intros a b n. bitwise as m. destruct (le_gt_cases n m). - rewrite !lnot_spec_high, lxor_spec; trivial. - rewrite !lnot_spec_low, lxor_spec, negb_xorb_r; trivial. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog