proposition: Lemma firstn_skipn_rev: forall x l, firstn x l = rev (skipn (length l - x) (rev l)).
proof: Proof. intros x l; rewrite <-(firstn_skipn x l) at 3. rewrite rev_app_distr, skipn_app, rev_app_distr, rev_length, skipn_length, Nat.sub_diag; simpl; rewrite rev_involutive. rewrite <-app_nil_r at 1; f_equal; symmetry; apply length_zero_iff_nil. repeat rewrite rev_length, skipn_length; apply Nat.sub_diag. Qed.
imports: PeanoNat