proposition: Lemma refine_M_hrel_find : refines (eq ==> M_hrel ==> option_R rAC) (@M.find A) (@M.find C).
proof: Proof. apply refines_abstr => k k'; rewrite refinesE => <-. apply refines_abstr => m m'; rewrite refinesE => ref_m. rewrite refinesE; case_eq (M.find k m') => [e'|]; case_eq (M.find k m) => [e|] /=. { move/F.find_mapsto_iff => H1 /F.find_mapsto_iff => H2. by constructor; apply (snd ref_m) with k. } { move/F.not_find_in_iff => H' H''; exfalso; apply H'. by apply (fst ref_m); rewrite F.in_find_iff H''. } { move=> H' /F.not_find_in_iff => H''; exfalso; apply H''. apply/(fst ref_m k)/F.in_find_iff. by rewrite H'. } by move=> *; constructor. 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)