proposition: Lemma firstn_app_2 n: forall l1 l2, firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2.
proof: Proof. induction n as [| k iHk];intros l1 l2. - unfold firstn at 2. rewrite Nat.add_0_r, app_nil_r. rewrite firstn_app. rewrite Nat.sub_diag. unfold firstn at 2. rewrite app_nil_r. apply firstn_all. - destruct l2 as [|x xs]. * simpl. rewrite app_nil_r. apply firstn_all2. now apply Nat.le_add_r. * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). 1:now rewrite Nat.add_comm, Nat.add_sub. rewrite H0, firstn_all2; [reflexivity | now apply Nat.le_add_r]. Qed.
imports: PeanoNat