proposition: Lemma seq_S : forall len start, seq start (S len) = seq start len ++ [start + len].
proof: Proof. intros len start. change [start + len] with (seq (start + len) 1). rewrite <- seq_app. rewrite Nat.add_succ_r, Nat.add_0_r; reflexivity. Qed.
imports: PeanoNat