[STATEMENT]
lemma R\<^sub>N_0 [simp]: "R\<^sub>N 0 u l = return_pmf 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sub>N 0 u l = return_pmf 0
[PROOF STEP]
unfolding R\<^sub>N_def R_def SL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>f. steps {..<0} f 0 u l) (Pi_pmf.Pi_pmf {..<0} 0 (\<lambda>_. geometric_pmf p)) = return_pmf 0
[PROOF STEP]
by (auto simp add: steps.simps)