Library hydras.Ackermann.PAtheory

From Coq Require Import Ensembles List Arith Lia.

From hydras.Ackermann Require Import subAll folReplace folProp folLogic3 NN LNN2LNT.
From hydras.Ackermann Require Export PA.
From hydras.Ackermann Require Import NewNotations.
Import NNnotations.

#[local] Arguments apply _ _ _ : clear implicits.

Lemma paZeroOrSucc (t : Term):
 let nv := newVar (0 :: freeVarT t) in
 SysPrf PA (t = LNT.Zero ∨ exH nv, t = LNT.Succ (v#nv))%nt.
           Opaque eq_nat_dec.
           Transparent eq_nat_dec.
          Opaque eq_nat_dec.
          Transparent eq_nat_dec.

Lemma paPlusSym : ∀ a b : Term,
    SysPrf PA (a + b = b + a)%nt.

Lemma NN72PA : SysPrf PA (LNN2LNT_formula NN7).

Lemma NN82PA : SysPrf PA (LNN2LNT_formula NN8).

Lemma NN92PA : SysPrf PA (LNN2LNT_formula NN9).