proposition: Lemma all_nth_coeff_eq_imp : forall p p' : RX, (forall i, nth_coeff i p [=] nth_coeff i p') -> p [=] p'.
proof: Proof. intro. induction p as [| s p Hrecp]; intros; [ induction p' as [| s p' Hrecp'] | induction p' as [| s0 p' Hrecp'] ]; intros. algebra. simpl in |- *. simpl in H. simpl in Hrecp'. split. apply eq_symmetric_unfolded. apply (H 0). apply Hrecp'. intros. apply (H (S i)). simpl in |- *. simpl in H. simpl in Hrecp. split. apply (H 0). change ([0] [=] (p:RX)) in |- *. apply eq_symmetric_unfolded. simpl in |- *. apply Hrecp. intros. apply (H (S i)). simpl in |- *. simpl in H. split. apply (H 0). change ((p:RX) [=] (p':RX)) in |- *. apply Hrecp. intros. apply (H (S i)). Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings