(*useful??*) Goal "(z = z + w) = (w = (#0::real))"; by Auto_tac; qed "real_add_left_cancel0"; Addsimps [real_add_left_cancel0];