proposition: Lemma list_nth_nil : forall A n (def : A), list_nth n nil def = def.
proof: Proof. intros A n def; induction n using Pos.peano_rect. + rewrite list_nth_base; reflexivity. + rewrite list_nth_succ; reflexivity. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia