proposition: Lemma degree_le_1_imp : forall p : RX, degree_le 1 p -> {a : R | {b : R | p [=] _C_ a[*]_X_[+]_C_ b}}.
proof: Proof. unfold degree_le in |- *. intros. exists (nth_coeff 1 p). exists (nth_coeff 0 p). apply all_nth_coeff_eq_imp. intros. elim i; intros. simpl in |- *. ring. elim n; intros. simpl in |- *. algebra. simpl in |- *. apply H. auto with arith. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia