[STATEMENT]
lemma a_mpi[simp]:"-\<infinity> + \<infinity>  = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<infinity> + \<infinity> = 0
[PROOF STEP]
apply (simp add:add_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse,
       simp add:Zero_ant_def ant_def zag_pl_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done