proposition: Corollary next_waypoint_b p b : terminating (p, (0, b)) + { '(p', b') | forall n, reaches_plus (p, (0, n+b)) (p', (0, n+b')) } + { '(p', (a', b')) | reaches (p, (0, b)) (p', (a', b')) /\ a' <= l /\ b' <= l }.
proof: Proof. have [[?|[[p' a'] Hp]]|[[p' b'] Hp]] := next_waypoint p 0 b. - left. by left. - right. exists (p', (a', 0)). have [k [? Hk]] := Hp 0. have ? := steps_bound Hk. split; [by exists k|lia]. - left. right. exists (p', b') => n. have [k [? Hk]] := Hp n. exists k. split; [lia|done]. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun