proposition: Lemma nth_middle : forall n l1 x l2, n = length l1 -> nth n (l1 ++ x :: l2) = x.
proof: Proof. Proof using. introv E. rewrite nth_app_r. { math_rewrite (n - length l1 = 0). rewrite~ nth_zero. } math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)