[STATEMENT]
lemma show_law_nat [show_law_intros]:
  "show_law showsp_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. show_law showsp_nat n
[PROOF STEP]
by (rule show_lawI, induct n rule: nat_less_induct) (simp add: show_law_simps showsp_nat.simps)