proposition: Theorem polynomial_nz_equiv : forall f, polynomial f -> polynomial_nz f.
proof: Proof. intuition. unfold polynomial, polynomial_nz in *. do 3 (destruct H). exists (S x). exists (S x0). exists (x0 + S x1). intuition. lia. rewrite H. rewrite Nat.add_assoc. eapply Nat.add_le_mono; intuition. simpl. destruct (eq_nat_dec x 0). subst. simpl. repeat rewrite Nat.mul_1_r. rewrite <- Nat.add_0_l at 1. eapply Nat.add_le_mono; intuition. rewrite <- Nat.add_0_l at 1. rewrite <- Nat.add_0_r at 1. eapply Nat.add_le_mono; intuition. eapply Nat.add_le_mono; intuition. eapply Nat.mul_le_mono; intuition. destruct (eq_nat_dec n 0); subst. rewrite expnat_0; lia. rewrite <- Nat.mul_1_l at 1. eapply Nat.mul_le_mono; intuition. lia. Qed.
imports: FCF.StdNat