proposition: Lemma cpoly_constant_strext : fun_strext (S1:=CR) (S2:=cpoly_cring) cpoly_constant.
proof: Proof. unfold fun_strext in |- *. unfold cpoly_constant in |- *. simpl in |- *. intros x y H. elim H. auto. intro. elim b. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational