proposition: Lemma mods_rec p q : mods p q = if p == 0 then [::] else p :: (mods q (next_mod p q)).
proof: Proof. rewrite /mods; set aux := fix aux _ _ n := if n is _.+1 then _ else _. have aux0 u n : aux 0 u n = [::] by case: n => [//|n] /=; rewrite eqxx. pose m p q := maxn (size p) (size q).+1; rewrite -!/(m _ _). suff {p q} Hnext p q : q != 0 -> (m q (next_mod p q) < m p q)%N; last first. rewrite /m -maxnSS leq_max !geq_max !ltnS leqnn /= /next_mod. rewrite size_scale ?oppr_eq0 ?lcn_neq0 //=. by move=> q_neq0; rewrite ltn_rmodp ?q_neq0 ?orbT. suff {p q} m_gt0 p q : (0 < m p q)%N; last by rewrite leq_max orbT. rewrite -[m p q]prednK //=; have [//|p_neq0] := altP (p =P 0). have [->|q_neq0] := altP (q =P 0); first by rewrite !aux0. congr (_ :: _); suff {p q p_neq0 q_neq0} Haux p q n n' : (m p q <= n)%N -> (m p q <= n')%N -> aux p q n = aux p q n'. by apply: Haux => //; rewrite -ltnS prednK // Hnext. elim: n p q n' => [p q|n IHn p q n' Hn]; first by rewrite geq_max ltn0 andbF. case: n' => [|n' Hn' /=]; first by rewrite geq_max ltn0 andbF. have [//|p_neq0] := altP eqP; congr (_ :: _). have [->|q_neq0] := altP (q =P 0); first by rewrite !aux0. by apply: IHn; rewrite -ltnS (leq_trans _ Hn, leq_trans _ Hn') ?Hnext. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)