proposition: Lemma refine_mnmd {n1} : refines (Rord0 ==> Rnat ==> Rseqmultinom) (@mnmd n1) (@mnmd_seq n1).
proof: Proof. case: n1 => [|n1]; first by rewrite refinesE => -[]. eapply refines_abstr => i i' ref_i. eapply refines_abstr => j j' ref_j. apply: refine_seqmultinomP. rewrite /mnmd_seq !(size_cat,size_nseq) /= -subnDA addnA addn1 subnKC //. by move: ref_i; rewrite refinesE /Rord0; move<-. move=> k. rewrite /mnmd_seq /mnmd multinomE (tnth_nth 0%N) /=. rewrite !(nth_cat,nth_nseq). rewrite (nth_map ord0); last by rewrite size_enum_ord. case: ifP. rewrite if_same size_nseq nth_enum_ord //. move=> Hic; rewrite ifF //. apply/negP; move/eqP => Keq. move/Rord0_eq in ref_i. by rewrite -ref_i -Keq ltnn in Hic. move/negbT; rewrite size_nseq -ltnNge ltnS => Hi. rewrite nth_enum_ord //. case: ifP. move/eqP <-; move/Rord0_eq: ref_i <-. rewrite subnn /=. have->: j = spec_id j by []. symmetry; eapply refinesP; refines_apply. move/negbT/eqP => Hneq. move/Rord0_eq in ref_i; rewrite -ref_i in Hi *. case: (ltnP i k) => Hci. by rewrite -(@prednK (k - i)) ?subn_gt0 //= nth_nseq if_same. by exfalso; apply/Hneq/anti_leq; rewrite Hi. 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)