proposition: Theorem append_correct2 : forall (s1 s2 : string) (n : nat), get n s2 = get (n + length s1) (s1 ++ s2).
proof: Proof. intros s1; elim s1; simpl; auto. - intros s2 n; rewrite Nat.add_comm; simpl; auto. - intros a s1' Rec s2 n; case n; simpl; auto. intros. (replace (n0 + S (length s1')) with (S n0 + length s1') by now rewrite Nat.add_succ_r); auto. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte