proposition: Lemma monic_c_one : monic 0 (_C_ ([1]:R)).
proof: Proof. unfold monic in |- *. intros. split. simpl in |- *. algebra. apply degree_le_c_. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia