proposition: Lemma bigmaxf_rec f n : \max_(i < n.+1) f i = Num.max (f n) (\max_(i < n) f i).
proof: Proof. move: f. elim: n => [ f /=|s Hrec f]; first by rewrite big_ord_recl big_ord0 big_ord0. symmetry; rewrite big_ord_recl maxCA big_ord_recl. pose g i := f i.+1. have aux: forall k, \max_(i < k) f (lift ord0 i) = (\max_(i < k) g i). move=> k; apply: eq_big => // i. by rewrite aux aux Hrec. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)