proposition: Lemma lead_coeff_product_1 (n: nat) (l: list (cpoly R)): (forall p, In p l -> (nth_coeff n p [=] [1] /\ degree_le n p)) -> nth_coeff (length l * n) (cr_Product l) [=] [1].
proof: Proof. Proof with auto. intro H. induction l. simpl. reflexivity. change (nth_coeff (n + length l * n) (a [*] cr_Product l)[=][1]). rewrite degree_mult_aux. setoid_replace (nth_coeff n a) with ([1]:R). rewrite IHl. apply mult_one. intros. apply H... apply H... apply H... apply degree_le_Product. intros. apply H... Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia