[STATEMENT]
lemma Infinitesimal_add_right_cancel: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> z + y \<Longrightarrow> x \<approx> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> Infinitesimal; x \<approx> z + y\<rbrakk> \<Longrightarrow> x \<approx> z
[PROOF STEP]
by (metis Infinitesimal_add_approx_self approx_monad_iff)