proposition: Lemma lnot_involutive : forall a n, lnot (lnot a n) n == a.
proof: Proof. intros a n. bitwise as m. destruct (le_gt_cases n m). - now rewrite 2 lnot_spec_high. - now rewrite 2 lnot_spec_low, negb_involutive. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog