proposition: Lemma skipn_skipn : forall x y l, skipn x (skipn y l) = skipn (x + y) l.
proof: Proof. intros x y. rewrite Nat.add_comm. induction y as [|y IHy]. - reflexivity. - intros [|]. + now rewrite skipn_nil. + now rewrite skipn_cons, IHy. Qed.
imports: PeanoNat