proposition: Lemma lt_i_lth_of_poly : forall i (p : RX), nth_coeff i p [#] [0] -> i < lth_of_poly p.
proof: Proof. intros i. induction i as [| i Hreci]; intros; rename X into H. induction p as [| s p Hrecp]; intros. simpl in H. elim (ap_irreflexive_unfolded _ _ H). simpl in |- *. auto with arith. induction p as [| s p Hrecp]; intros. simpl in H. elim (ap_irreflexive_unfolded _ _ H). simpl in |- *. simpl in H. apply -> Nat.succ_lt_mono. auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia