proposition: Lemma largest_of_depth_monotone: forall n1 n2, n1 <= n2 -> eval (largest_of_depth n1) <= eval (largest_of_depth n2).
proof: Proof. intros. unfold largest_of_depth. eapply (maxBy_monotone eval (termsUpTo n1) (termsUpTo n2)). 2: reflexivity. intros. eapply termsUpTo_correct. eapply termsUpTo_correct in H0. eapply Nat.le_trans; eassumption. Qed.
imports: Arith Lia List FunctionalExtensionality