proposition: Lemma sorted_filter (s : seq nat) (p : pred nat) : sorted s -> sorted (filter p s).
proof: Proof. have F a s1 i : sorted (a :: s1) -> i < size (filter p s1) -> a < nth 0 (filter p s1) i. elim: s1 i => //= b s1 IH i abS. have [pbT|pbF] := boolP (p b). case: i => [|i1] /= sH; first by rewrite (abS 0 1). apply: IH => //. by apply: sorted_skip abS. apply: IH. by apply: sorted_skip abS. elim: s => //= a s IH aS. have sS := sorted_cons aS. have [paT|paF] := boolP (p a); last by apply: IH. move=> [|i] [|j] iH jH /=. - by rewrite ltnn. - by rewrite F. - by rewrite ltnNge ltnW // F. by rewrite ltnS (IH sS). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)