proposition: Theorem polynomial_mult : forall f1 f2 , polynomial f1 -> polynomial f2 -> polynomial (fun n => f1 n * f2 n).
proof: Proof. intros f1 f2 H H0. apply polynomial_nz_equiv in H. apply polynomial_nz_equiv in H0. unfold polynomial, polynomial_nz in *. repeat des. intuition. exists (x + x2). exists (3 * (x3 * x0 * x4 * x1)). exists (x4 * x1). intros n. eapply Nat.le_trans. eapply Nat.mul_le_mono. eapply H6; intuition. eapply H7; intuition. repeat rewrite Nat.mul_add_distr_l. repeat rewrite Nat.mul_add_distr_r. rewrite Nat.add_assoc. eapply Nat.add_le_mono; trivial. rewrite expnat_plus. simpl. rewrite Nat.add_0_r. repeat rewrite Nat.mul_add_distr_r. rewrite Nat.add_assoc. eapply Nat.add_le_mono. eapply Nat.add_le_mono. rewrite (Nat.mul_comm (expnat n x)). repeat rewrite Nat.mul_assoc. eapply Nat.mul_le_mono. 2: reflexivity. rewrite Nat.mul_comm. rewrite Nat.mul_assoc. eapply Nat.mul_le_mono. 2: reflexivity. rewrite <- Nat.mul_1_r at 1. rewrite <- Nat.mul_1_r at 1. eapply Nat.mul_le_mono. 2: auto with zarith. eapply Nat.mul_le_mono. 2: auto with zarith. rewrite Nat.mul_comm. reflexivity. destruct (eq_nat_dec n 0); subst. repeat rewrite expnat_0. simpl. repeat rewrite Nat.mul_0_r. reflexivity. trivial. trivial. rewrite (Nat.mul_comm (expnat n x)). repeat rewrite Nat.mul_assoc. eapply Nat.mul_le_mono; trivial. rewrite <- Nat.mul_1_r at 1. eapply Nat.mul_le_mono; trivial. rewrite <- Nat.mul_1_r at 1. eapply Nat.mul_le_mono; trivial. rewrite Nat.mul_comm. eapply Nat.mul_le_mono; trivial. rewrite <- Nat.mul_1_l at 1. eapply Nat.mul_le_mono; trivial. eapply expnat_ge_1. lia. destruct (eq_nat_dec n 0); subst. repeat rewrite expnat_0. simpl. repeat rewrite Nat.mul_0_r. intuition. trivial. trivial. rewrite (Nat.mul_comm (expnat n x)). repeat rewrite Nat.mul_assoc. rewrite <- Nat.mul_1_r at 1. eapply Nat.mul_le_mono; trivial. rewrite <- Nat.mul_assoc. rewrite (Nat.mul_comm (expnat n x2)). rewrite Nat.mul_assoc. eapply Nat.mul_le_mono; trivial. eapply Nat.mul_le_mono; trivial. rewrite <- Nat.mul_1_r at 1. eapply Nat.mul_le_mono; trivial. rewrite <- Nat.mul_1_r at 1. eapply Nat.mul_le_mono; trivial. eapply expnat_ge_1. lia. Qed.
imports: FCF.StdNat