proposition: Lemma natNE (a b : nat) : a <> b -> SysPrf NN (natToTerm a <> natToTerm b)%fol.
proof: Proof. revert a b; assert (H: forall a b : nat, a < b -> SysPrf NN (natToTerm a <> natToTerm b)%fol). { induction a as [| a Hreca]; intros. - destruct b as [| n]. + elim (Nat.nlt_0_r _ H). + cbn; apply impE with (Succ (natToTerm n) <> Zero)%fol. * apply cp2, impI, eqSym. apply Axm; right; constructor. * apply nn1. - destruct b as [| n]. + elim (Nat.nlt_0_r _ H). + cbn; apply impE with (natToTerm a <> natToTerm n)%fol. * apply cp2, nn2. * apply Hreca; lia. } intros a b H0; destruct (Nat.lt_gt_cases a b) as [H1 _]; specialize (H1 H0); destruct H1 as [H1 | H1]. - now apply H. - apply impE with (natToTerm b <> natToTerm a)%fol. + apply cp2, impI, eqSym. apply Axm; right; constructor. + now apply H. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(folLogic3 folProp subProp) hydras.Ackermann(folLogic3 folProp subProp) hydras(Compat815)