proposition: Lemma steps_bound {k p a b p' a' b'} : steps k (p, (a, b)) = Some (p', (a', b')) -> a' <= k + a /\ b' <= k + b /\ (a' <= k \/ a <= k + a') /\ (b' <= k \/ b <= k + b').
proof: Proof. elim: k p' a' b'. { move=> p' a' b' /= []. lia. } move=> k + p' a' b' /=. case: (steps k (p, (a, b))) => [[p'' [a'' b'']]|]; last done. move=> /(_ p'' a'' b'' ltac:(done)) IH. rewrite /= /(step _). case: (nth_error M (state (p'', (a'', b'')))); last done. case. - done. - case; case; lia. - case; case; lia. - case => q /=. + move: b'' IH => [|b''] ? []; lia. + move: a'' IH => [|a''] ? []; lia. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun