fact: Definition pos_nxt_inj n (p q : pos n) (H : pos_nxt p = pos_nxt q) : p = q := match H in _ = a return match a as a' in pos m return match m with | 0 => Prop | S n' => pos n' -> Prop end with | pos_fst => fun _ => True | pos_nxt y => fun x' => x' = y end p with | eq_refl => eq_refl end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)