proposition: Lemma seq_app : forall len1 len2 start, seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2.
proof: Proof. intro len1; induction len1 as [|len1' IHlen]; intros; simpl in *. - now rewrite Nat.add_0_r. - now rewrite Nat.add_succ_r, IHlen. Qed.
imports: PeanoNat