proposition: Lemma mnmc_eq_seqP s1 s2 : reflect (mnmc_eq_seq s1 s2) (s1 == s2).
proof: Proof. move: s2; elim s1 => {s1}[|a1 s1 Hind] s2. { now case s2 => [|n l]; apply (iffP idP). } case s2 => {s2}[|a2 s2]; [by apply (iffP idP)|]. specialize (Hind s2); rewrite /mnmc_eq_seq /=; apply (iffP idP). { move/eqP => [Hs Ha]; rewrite Hs Rnat_eqxx /=. exact/Hind/eqP. } by move/andP => [Ha Hs]; apply/eqP; f_equal; apply /eqP => //; apply/Hind. Qed.
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)