proposition: Lemma degree_le_c_ : forall c : R, degree_le 0 (_C_ c).
proof: Proof. unfold degree_le in |- *. intros c m. elim m; intros. elim (Nat.lt_irrefl _ H). simpl in |- *. algebra. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia