proposition: Lemma degree_le_x_ : degree_le 1 (_X_:RX).
proof: Proof. unfold degree_le in |- *. intro. elim m. intros. elim (Nat.nlt_0_r _ H). intro. elim n. intros. elim (Nat.lt_irrefl _ H0). intros. simpl in |- *. algebra. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia