proposition: Lemma nth_app_right : forall (l m: list A) i, i >= length l -> nth_error (l ++ m) i = nth_error m (i - length l).
proof: Proof. induction l; simpl; intros m i i_l. auto with arith. destruct i; simpl. lia. apply IHl. auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)