proposition: Lemma nth_last_case : forall n x l, nth n (l&x) = (If n = length l then x else nth n l).
proof: Proof. Proof using. intros. case_if. { rewrite nth_app_r; [|math]. math_rewrite (n-length l = 0). rewrite~ nth_zero. } { tests C': (n < length l). { rewrite~ nth_app_l. } { rewrite nth_gt_length; [|rew_list; math]. rewrite nth_gt_length; [|math]. auto. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)