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 n m) || (idtac "step0 test3 fails"; induction n). all: (simpl; congruence). Qed.
imports: Autoinduct(Autoinduct)