proposition: Lemma skipn_app_R : forall T n (a b : list T), length a <= n -> skipn n (a ++ b) = skipn (n - length a) b.
proof: Proof. induction n; destruct a; simpl in *; intros; auto. exfalso; lia. eapply IHn. lia. Qed.
imports: Coq.Lists.List Coq.ZArith.ZArith Coq.micromega.Lia