proposition: Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x.
proof: Proof. intros A n; induction n using Pos.peano_rect; intros x def; simpl. + reflexivity. + unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def). rewrite list_nth_succ; auto. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia