proposition: Theorem polynomial_plus : forall f1 f2 , polynomial f1 -> polynomial f2 -> polynomial (fun n => f1 n + f2 n).
proof: Proof. intuition. apply polynomial_nz_equiv in H. apply polynomial_nz_equiv in H0. unfold polynomial, polynomial_nz in *. Ltac des := match goal with | [H : exists _, _ |- _] => destruct H end. repeat des. intuition. exists (max x2 x). exists (x3 + x0). exists (x4 + x1). intuition. eapply Nat.le_trans. eapply Nat.add_le_mono. eapply H6; trivial. eapply H7; trivial. rewrite Nat.mul_add_distr_r. repeat rewrite Nat.add_assoc. eapply Nat.add_le_mono; trivial. rewrite Nat.add_comm. rewrite Nat.add_assoc. eapply Nat.add_le_mono; trivial. rewrite Nat.add_comm. eapply Nat.add_le_mono; eapply Nat.mul_le_mono; intuition. eapply expnat_exp_le; intuition. eapply expnat_exp_le; intuition. Qed.
imports: FCF.StdNat