[STATEMENT]
lemma ord_of_nat_add: "ord_of_nat (m+n) = ord_of_nat m + ord_of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_of_nat (m + n) = ord_of_nat m + ord_of_nat n
[PROOF STEP]
by (induction n) (auto simp: plus_V_succ_right)