[STATEMENT]
lemma prv_eql_pls_plus:
"prv (eql (pls (Num m) (Num n))
          (Num (m+n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eql (pls (Num m) (Num n)) (Num (m + n)))
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
 2. \<And>n. prv (eql (pls (Num m) (Num n)) (Num (m + n))) \<Longrightarrow> prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
prv (eql (pls (Num m) (Num n)) (Num (m + n)))

goal (2 subgoals):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
 2. \<And>n. prv (eql (pls (Num m) (Num n)) (Num (m + n))) \<Longrightarrow> prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
note 0 = prv_pls_suc[of "Num m" "Num n", simplified]
[PROOF STATE]
proof (state)
this:
prv (eql (pls (Num m) (suc (Num n))) (suc (pls (Num m) (Num n))))

goal (2 subgoals):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
 2. \<And>n. prv (eql (pls (Num m) (Num n)) (Num (m + n))) \<Longrightarrow> prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
by (auto intro: prv_eql_trans[OF _ _ _ 0 prv_suc_cong[OF _ _ Suc]])
[PROOF STATE]
proof (state)
this:
prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))

goal (1 subgoal):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
[PROOF STEP]
qed(simp add: prv_pls_zer)