proposition: Lemma cpoly_cr_non_triv : cpoly_ap cpoly_one cpoly_zero.
proof: Proof. change (cpoly_linear_cs [1] cpoly_zero_cs [#] cpoly_zero_cs) in |- *. cut (([1]:CR) [#] [0] or cpoly_zero_cs [#] cpoly_zero_cs). auto. left. algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational