proposition: Lemma natLT (a b : nat): a < b -> SysPrf NN (natToTerm a < natToTerm b)%fol.
proof: Proof. intros H; eapply orE. - apply nn9 with (a := natToTerm b) (b := natToTerm a). - apply impI; apply contradiction with (natToTerm b < natToTerm a)%fol. + apply Axm; right; constructor. + now apply sysWeaken, natLE, Nat.lt_le_incl. - apply impI, orSys. + apply contradiction with (natToTerm b = natToTerm a)%fol. * apply Axm; right; constructor. * apply sysWeaken, natNE. unfold not in |- *; intros. subst; lia. + apply Axm; right; constructor. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(folLogic3 folProp subProp) hydras.Ackermann(folLogic3 folProp subProp) hydras(Compat815)