fact: Fixpoint mnmc_lt_seq_aux (s1 s2 : seq binnat.N) {struct s1} : bool := match s1, s2 with | [::], [::] => false | [::], _ => true | x1 :: s1', [::] => false | x1 :: s1', x2 :: s2' => (x1 < x2)%C || (x1 == x2)%C && mnmc_lt_seq_aux s1' s2' 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)