proposition: Lemma reaches_plus_state_bound {x y} : reaches_plus x y -> state x < l.
proof: Proof. move=> [k [? Hk]]. suff: not (l <= state x) by lia. move=> /nth_error_None Hx. move: Hk. have ->: k = S (k - 1) by lia. by rewrite /= obind_oiter /step Hx oiter_None. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun