proposition: Lemma nth_app : forall n l1 l2, nth n (l1 ++ l2) = If (n < length l1) then (nth n l1) else (nth (n - length l1) l2).
proof: Proof. Proof using. intros. case_if. { applys~ nth_app_l. } { applys nth_app_r; math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)