fact: Definition compare (x y : t) : Compare lt eq x y := match sumb (mnmc_lt_seq x y) with | left prf => LT prf | right prf => match sumb (mnmc_lt_seq y x) with | left prf' => GT prf' | right prf' => EQ (intro_eq prf prf') end end.
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)