proposition: Lemma skipn_rev: forall x l, skipn x (rev l) = rev (firstn (length l - x) l).
proof: Proof. intros x l; rewrite firstn_skipn_rev, rev_involutive, <-rev_length. destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. now rewrite L, Nat.sub_0_r, skipn_all. - f_equal. now apply Nat.eq_sym, Nat.add_sub_eq_l, Nat.sub_add. Qed.
imports: PeanoNat