proposition: Lemma degree_c_ : forall c : R, c [#] [0] -> degree 0 (_C_ c).
proof: Proof. unfold degree in |- *. intros. split. simpl in |- *. auto. apply degree_le_c_. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia