proposition: Lemma cpoly_is_CSetoid : is_CSetoid _ cpoly_eq cpoly_ap.
proof: Proof. apply Build_is_CSetoid. exact irreflexive_cpoly_ap. exact symmetric_cpoly_ap. exact cotransitive_cpoly_ap. exact tight_apart_cpoly_ap. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational