proposition: Lemma sorted_skip a b s : sorted (a :: b :: s) -> sorted (a :: s).
proof: Proof. move=> Hs [|i] [|j] iH jH //=; first by rewrite ltnn. - by rewrite (Hs 0 j.+2). - by rewrite (Hs i.+2 0). by rewrite (Hs i.+2 j.+2). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)