proposition: Lemma lead_coef_prod (s : seq {poly R}) : \prod_(p <- s) lead_coef p = lead_coef (\prod_(p <- s) p).
proof: Proof. elim: s=> [|a l IHl]; first by rewrite !big_nil lead_coef1. by rewrite !big_cons lead_coefM -IHl. Qed.
imports: mathcomp(all_ssreflect all_algebra)