proposition: Lemma add_lnot_diag_low : forall a n, log2 a < n -> a + lnot a n == ones n.
proof: Proof. intros a n H. assert (H' := land_lnot_diag_low a n H). rewrite add_nocarry_lxor, lxor_lor by trivial. now apply lor_lnot_diag_low. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog