proposition: Lemma cpoly_x_minus_c_strext : fun_strext (S1:=CR) (S2:=cpoly_cring) cpoly_x_minus_c.
proof: Proof. unfold fun_strext in |- *. unfold cpoly_x_minus_c in |- *. simpl in |- *. intros x y H. elim H; intro H0. apply (cs_un_op_strext _ _ _ _ H0). elim H0; intro H1. elim (ap_irreflexive_unfolded _ _ H1). elim H1. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational