Library hydras.Ackermann.NNtheory

From Coq Require Import Arith Lia.

From hydras.Ackermann Require Import folLogic3 folProp subProp.
From hydras.Ackermann Require Import folLogic3 folProp subProp.
From hydras.Ackermann Require Export NN.
From hydras Require Import Compat815.
Import NNnotations.

Lemma natNE (a b : nat) :
  a ≠ b → SysPrf NN (natToTerm a ≠ natToTerm b)%fol.

Lemma natLE (a b : nat):
 b ≤ a → SysPrf NN (¬ (natToTerm a < natToTerm b))%fol.

Lemma natLT (a b : nat):
  a < b → SysPrf NN (natToTerm a < natToTerm b)%fol.

Lemma natPlus (a b : nat):
 SysPrf NN (natToTerm a + natToTerm b = natToTerm (a + b)%nat)%fol.

Lemma natTimes (a b : nat):
 SysPrf NN (natToTerm a ×natToTerm b = natToTerm (a × b)%nat)%fol.

Lemma boundedLT (m : nat) (a : Formula) (x : nat):
  (∀ n : nat,
      n < m → SysPrf NN (substF a x (natToTerm n))) →
  SysPrf NN (v#x < natToTerm m → a)%fol.

Lemma nnPlusNotNeeded (n:nat) :
 SysPrf NN
 (v#1 < natToTerm n ∨ v#1 = natToTerm n →
  v#1 < S_ (natToTerm n))%fol.