proposition: Lemma nth_app_r : forall n l1 l2, n >= length l1 -> nth n (l1 ++ l2) = nth (n - length l1) l2.
proof: Proof. Proof using. unfold nth. intros n l1. gen n. induction l1; introv N; rew_list in *. { fequals; math. } { destruct n as [|n']. { false; math. } unfold nth_default; fold nth_default. simpl. rewrite IHl1; [|math]. fequals; math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)