proposition: Lemma loop_a {p a a' b} : a <= a' -> (forall n : nat, reaches_plus (p, (n + a, b)) (p, (n + a', b))) -> non_terminating (p, (a, b)).
proof: Proof. move=> ? Hp k. suff: forall m, steps k (p, (m + a, b)) <> None by move=> /(_ 0). elim: k; first done. move=> k IH m. have [k' [? Hk']] := Hp m. move=> /(steps_k_monotone (k' + k)) /(_ ltac:(lia)). move: Hk' => /steps_plus ->. have ->: m + a' = (m + a' - a) + a by lia. by apply: IH. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun