Appears in collection : Francophone Computer Algebra Days - 2026 / JNCF - Journées nationales de calcul formel - 2026

We have long known how to prove identities between sequences defined by linear recurrences with polynomial coefficients, but the development of algorithms proving inequalities is relatively recent. Inequalities, or even simply positivity, are actually delicate questions related to problems whose decidability is still unknown, even for recurrences with constant coefficients. This course will present recent algorithms that cover a large class of linear recurrences. These algorithms construct proofs by induction that take the form of cones that are stable by an underlying recurrence operator. The existence and construction of such cones rely on an extension of the classical Perron- Frobenius theory to matrices leaving a cone invariant. The more recent parts of the course are based on joint work with Alaa Ibrahim.