fact: Definition mods p q := let fix aux p q n := if n is m.+1 then if p == 0 then [::] else p :: (aux q (next_mod p q) m) else [::] in aux p q (maxn (size p) (size q).+1).
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)