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