proposition: Lemma suppE (s1 s2 : fmap) : supp s1 =i supp s2 <-> supp s1 = supp s2.
proof: Proof. split; last by move=>->. case: s1 s2=>s1 H1 [s2 H2]; rewrite /supp /=. elim: s1 s2 H1 H2=>[|[k1 _] s1 IH][|[k2 _] s2] //=. - by move=>_ _; move/(_ k2); rewrite inE eq_refl. - by move=>_ _; move/(_ k1); rewrite inE eq_refl. case: (ordP k1 k2)=>/= O H1 H2. - move/(_ k1); rewrite !inE eq_refl /= eq_sym. case: ordP O => //= O _. by move/(ord_path O)/notin_path/negbTE: H2=>->. - rewrite -{k2 O}(eqP O) in H1 H2 *. move=>H; congr (_ :: _); apply: IH. - by apply: path_sorted H1. - by apply: path_sorted H2. move=>x; move: (H x); rewrite !inE /=. case: eqP=>// -> /= _. by move/notin_path/negbTE: H1=>->; move/notin_path/negbTE: H2=>->. move/(_ k2); rewrite !inE eq_refl /= eq_sym. case: ordP O=>//= O _. by move/(ord_path O)/notin_path/negbTE: H1=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)