proposition: Lemma poly_extensional : forall p q : RX, (forall x, p ! x [=] q ! x) -> p [=] q.
proof: Proof. intros p q H0. apply cg_inv_unique_2. apply not_ap_imp_eq. unfold Not in |- *. intros H1. elim (poly_apzero (p[-]q)). intros x H2. cut ((p[-]q) ! x [=] [0]). intro. elim (eq_imp_not_ap _ _ _ H3 H2). astepl (p ! x[-]q ! x). Step_final (p ! x[-]p ! x). auto. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation