proposition: Lemma loweqP h1 h2 : reflect (ldom h1 =i ldom h2) (h1 =~ h2).
proof: Proof. case E: (loweq h1 h2); constructor; rewrite /loweq in E. - by move=>x; rewrite /ldom (eqP E). move=>F. suff {E} : get_lows h1 = get_lows h2 by move/eqP; rewrite E. apply: ord_sorted_eq; last by apply: F. case: h1 {F}=>// [[h S] H]. by rewrite sorted_filter //; apply: trans. case: h2 {F}=>// [[h S] H]. by rewrite sorted_filter //; apply: trans. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep