proposition: Lemma add_left_S : forall (n m : nat), S (add_left n m) = add_left n (S m).
proof: Proof. intros. autoinduct on add_left || (idtac "step1 test3 fails"; induction n). all: (simpl; congruence). Qed.
imports: Autoinduct(Autoinduct)