proposition: Lemma path_supp_ord (s : fmap) k : path ord k (supp s) -> forall m, m \in supp s -> ord k m.
proof: Proof. case: s=>s H; rewrite /supp /= => H1 m H2; case: totalP H1 H2=>//. - by move=>H1 H2; move: (notin_path (ord_path H1 H2)); case: (m \in _). by move/eqP=>->; move/notin_path; case: (k \in _). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)