proposition: Lemma degree_le_mon : forall (p : RX) m n, m <= n -> degree_le m p -> degree_le n p.
proof: Proof. unfold degree_le in |- *. intros. apply H0. apply Nat.le_lt_trans with n; auto with arith. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia