fact: Definition list_nth {A} p (l : list A) def := Pos.peano_rect (fun _ => list A -> A) (fun l => match l with nil => def | cons t l => t end) (fun _ F l => match l with nil => def | cons t l => F l end) p l.
imports: Bool PArith DecidableClass Ring Lia