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