proposition: Lemma next_small_waypoint p a b : terminating (p, (a, b)) + non_terminating (p, (a, b)) + { '(p', (a', b')) | reaches_plus (p, (a, b)) (p', (a', b')) /\ a' <= l /\ b' <= l }.
proof: Proof. have [[?|[[p' a'] Hp]]|[[p' b'] Hp]] := next_waypoint p a b. - left. by left. - have [[|]|] := big_wf_a p' a' (fun _ => None) ltac:(done). * move=> /reaches_terminating Hp'. left. left. apply: Hp'. have [k [? Hk]] := Hp 0. by exists k. * move=> /reaches_non_terminating Hp'. left. right. apply: Hp'. have [k [? Hk]] := Hp 0. by exists k. * move=> [[p'' [a'' b'']]] [Hp'] ?. right. exists (p'', (a'', b'')). split; last done. apply: (reaches_plus_reaches _ Hp'). have [k [? Hk]] := Hp 0. exists k. split; [lia|done]. - have [[|]|] := big_wf_b p' b' (fun _ => None) ltac:(done). * move=> /reaches_terminating Hp'. left. left. apply: Hp'. have [k [? Hk]] := Hp 0. by exists k. * move=> /reaches_non_terminating Hp'. left. right. apply: Hp'. have [k [? Hk]] := Hp 0. by exists k. * move=> [[p'' [a'' b'']]] [Hp'] ?. right. exists (p'', (a'', b'')). split; last done. apply: (reaches_plus_reaches _ Hp'). have [k [? Hk]] := Hp 0. exists k. split; [lia|done]. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun