proposition: Lemma pos_nthe x A n : pos x A = Some n -> nthe n A = Some x.
proof: Proof. revert n. induction A as [|y A IH]; cbn; intros n. - intros [=]. - destruct (d x y) as [<-|H1]. + now intros [= <-]. + destruct (pos x A) as [k|]; intros [= <-]; cbn. now apply IH. Qed.
imports: List Lia Undecidability.PCP.PCP