proposition: Lemma cpolyap_strext : forall (f : RX) x y, f ! x [#] f ! y -> x [#] y.
proof: Proof. intros f x y H. elim (csbf_strext _ _ _ _ _ _ _ _ H); intro H0. elim (ap_irreflexive_unfolded _ _ H0). assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational