proposition: Lemma nth_coeff_strext : forall n p p', nth_coeff n p [#] nth_coeff n p' -> p [#] p'.
proof: Proof. do 3 intro. generalize n. clear n. pattern p, p' in |- *. apply Ccpoly_double_sym_ind. unfold Csymmetric in |- *. intros. apply ap_symmetric_unfolded. apply X with n. apply ap_symmetric_unfolded. assumption. intro p0. pattern p0 in |- *. apply Ccpoly_induc. simpl in |- *. intros. elim (ap_irreflexive_unfolded _ _ X). do 4 intro. elim n. simpl in |- *. auto. intros. cut (c [#] [0] or p1 [#] [0]). intro; apply _linear_ap_zero. auto. right. apply X with n0. astepr ([0]:R). auto. intros. induction n as [| n Hrecn]. simpl in X0. cut (c [#] d or p0 [#] q). auto. auto. cut (c [#] d or p0 [#] q). auto. right. apply X with n. exact X0. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings