proposition: Lemma lor_lnot_diag : forall a n, lor a (lnot a n) == lor a (ones n).
proof: Proof. intros a n. bitwise as m. destruct (le_gt_cases n m). - rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m]. - rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m]. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog