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