proposition: Lemma prod_all_ge0 (p : {poly R}) (q : {poly R}) : p != 0 -> q != 0 -> (forall i, (i <= (size p).-1)%N -> 0 < p`_i) -> (forall j, (j <= (size q).-1)%N -> 0 < q`_j) -> forall k, (k <= (size (p * q)%R).-1)%N -> 0 < (p * q)`_k.
proof: Proof. wlog: p q / ((size p).-1 <= (size q).-1)%N => H Hp Hq Hpcoef Hqcoef k Hk. case/orP : (leq_total (size p).-1 (size q).-1) => H2. by apply: H. rewrite mulrC; rewrite mulrC in Hk. by apply: (H q p H2). case : (leqP k (size p).-1) => Hk2. rewrite coefM (bigD1 ord0) //= subn0 (lt_le_trans (y := (p`_0 * q`_k))) //. rewrite pmulr_lgt0; first by rewrite Hpcoef. by rewrite Hqcoef // (@leq_trans ((size p).-1)). rewrite ler_addl sumr_ge0 //. case => /= i Hi Hi2. rewrite pmulr_rge0. case Hki : (k - i <= (size q).-1)%N. by rewrite ltW // Hqcoef. rewrite le0r -{1}(coefK q) coef_poly /=. have Hki2 : ((k - i < (size q))%N = false). by rewrite -[(size q)]prednK ?ltnS // size_poly_gt0. by rewrite Hki2 eq_refl. by rewrite Hpcoef // (leq_trans (n:=k)). rewrite coefM. have Hk3 : ((size p).-1 < k.+1)%N by apply: (ltn_trans (n:=k)). rewrite (bigD1 (Ordinal Hk3)) //= (lt_le_trans (y := (p`_(size p).-1 * q`_(k - (size p).-1)))) //. have Hk4: (k - (size p).-1 <= (size q).-1)%N. rewrite leq_subLR. by rewrite size_mul // -[size p]prednK ?size_poly_gt0 // -[size q]prednK ?size_poly_gt0 // addSn addnS -!pred_Sn in Hk. rewrite pmulr_rgt0; first by rewrite Hqcoef. by apply: Hpcoef. rewrite ler_addl sumr_ge0 //. case => /= i Hi Hi2. apply: mulr_ge0. case Hi3 : (i <= (size p).-1)%N. by rewrite ltW // Hpcoef. rewrite le0r -{1}(coefK p) coef_poly /=. rewrite ifF ?eqxx//. by rewrite -[(size p)]prednK ?ltnS // size_poly_gt0. case Hki : (k - i <= (size q).-1)%N. by rewrite ltW // Hqcoef. rewrite le0r -{1}(coefK q) coef_poly /=. rewrite ifF ?eqxx//. by rewrite -[(size q)]prednK ?ltnS // size_poly_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)