proposition: Lemma add_left_comm: forall (n m : nat), add_left n m = add_left m n.
proof: Proof. intros. autoinduct on add_left || (idtac "step1 test5 fails"; induction n). all: simpl. - symmetry. apply add_left_O. - (rewrite IHn || rewrite IHn0). apply add_left_S. Qed.
imports: Autoinduct(Autoinduct)