proposition: Lemma size_prod_eq1 (sq : seq {poly R}) : reflect (forall q, q \in sq -> size q = 1%N) (size (\prod_(q0 <- sq) q0) == 1%N).
proof: Proof. apply: (iffP idP). elim: sq => [| q sq ih]; first by move=> _ q; rewrite in_nil. rewrite big_cons; case: (altP (q =P 0)) => [-> | qn0]. by rewrite mul0r size_poly0. case: (altP ((\prod_(j <- sq) j) =P 0)) => [-> | pn0]. by rewrite mulr0 size_poly0. rewrite size_mul //; case: (ltngtP (size q) 1). - by rewrite ltnS leqn0 size_poly_eq0 (negPf qn0). - case: (size q) => [|n] //; case: n => [|n] // _; rewrite !addSn /= eqSS. by rewrite addn_eq0 size_poly_eq0 (negPf pn0) andbF. - move=> sq1; case: (ltngtP (size (\prod_(j <- sq) j)) 1). + by rewrite ltnS leqn0 size_poly_eq0 (negPf pn0). + case: (size (\prod_(j <- sq) j)) => [|n] //; case: n => [|n] // _. by rewrite !addnS /= eqSS addn_eq0 size_poly_eq0 (negPf qn0). move=> sp1 _ p; rewrite in_cons; case/orP => [/eqP -> |] //; apply: ih. by apply/eqP. elim: sq => [| q sq ih] hs; first by rewrite big_nil size_poly1 eqxx. case: (altP (q =P 0)) => [ | qn0]. by move/eqP; rewrite -size_poly_eq0 hs ?mem_head. case: (altP ((\prod_(q0 <- sq) q0) =P 0)) => [ | pn0]. move/eqP; rewrite -size_poly_eq0 (eqP (ih _)) // => t ht; apply: hs. by rewrite in_cons ht orbT. rewrite big_cons size_mul // (eqP (ih _)) //; last first. by move=> t ht; apply: hs; rewrite in_cons ht orbT. by rewrite addnS addn0; apply/eqP; apply: hs; apply: mem_head. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)