[STATEMENT]
lemma ord_spmf_map_spmf1: "ord_spmf R (map_spmf f p) = ord_spmf (\<lambda>x. R (f x)) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf R (map_spmf f p) = ord_spmf (\<lambda>x. R (f x)) p
[PROOF STEP]
by(simp add: pmf.rel_map[abs_def] ord_option_map1[abs_def])