proposition: Lemma identical_poly : (forall i j: nat, i <= n -> j <= n -> i <> j -> a_ i[#]a_ j) -> forall f g : RX, degree_le n f -> degree_le n g -> (forall i, i <= n -> f ! (a_ i) [=] g ! (a_ i)) -> f [=] g.
proof: Proof. intros. apply cg_inv_unique_2. apply zero_poly with n. assumption. apply degree_le_minus; auto. intros. astepl (f0 ! (a_ i) [-]g ! (a_ i)). Step_final (f0 ! (a_ i) [-]f0 ! (a_ i)). Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation