proposition: Lemma refine_M_hrel_add : refines (eq ==> rAC ==> M_hrel ==> M_hrel) (@M.add A) (@M.add C).
proof: Proof. rewrite refinesE => m _ <- a c Hac x x' Hx; split. { move=> k; rewrite !F.add_in_iff; split; by rewrite (fst Hx k). } move=> k e e' H1 H2. apply add_mapsto_iff_dec in H1. apply add_mapsto_iff_dec in H2. move: H1 H2. case=> [[Hy <-]|[Hy He]]. { move: Hy; move/mnmc_eq_seqP/eqP->. elim=>[[_ <-]|] // []; rewrite -/(E.eq k k) => K; exfalso; apply: K. exact: E.eq_refl. } by case; [elim=> H'; elim (Hy H')|elim=>_; apply (snd Hx)]. 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)