fact: Definition list_of_mpoly {R : ringType} {n} (p : {mpoly R[n]}) : seq ('X_{1..n} * R) := [seq (m, p@_m) | m <- path.sort mnmc_le (msupp p)].
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)