proposition: Lemma add_lnot_diag : forall a, a + lnot a == -1.
proof: Proof. intros a. unfold lnot. now rewrite add_pred_r, add_opp_r, sub_diag, one_succ, opp_succ, opp_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog