proposition: Lemma natLE (a b : nat): b <= a -> SysPrf NN (~ (natToTerm a < natToTerm b))%fol.
proof: Proof. intros H; induction b as [| b Hrecb]. - apply nn7. - cbn; apply impE with (~ (natToTerm a < natToTerm b \/ natToTerm a = natToTerm b))%fol. + apply cp2, nn8. + apply nOr, andI. * apply Hrecb; lia. * apply natNE. intro H0; lia. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(folLogic3 folProp subProp) hydras.Ackermann(folLogic3 folProp subProp) hydras(Compat815)