proposition: Lemma list_nth_succ : forall A n (def : A) l, list_nth (Pos.succ n) l def = match l with nil => def | cons _ l => list_nth n l def end.
proof: Proof. intros A def l; unfold list_nth. rewrite Pos.peano_rect_succ; reflexivity. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia