proposition: Remark maxLemma3 : forall a b : list nat, fold_right Nat.max 0 b <= fold_right Nat.max 0 (a ++ b).
proof: Proof. intros a b; induction a as [| a a0 Hreca]. - apply le_n. - simpl; apply Nat.le_trans with (fold_right Nat.max 0 (a0 ++ b)). + assumption. + apply Nat.le_max_r. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)