proposition: Lemma loop_b {p a b b'} : b <= b' -> (forall n : nat, reaches_plus (p, (a, n + b)) (p, (a, n + b'))) -> non_terminating (p, (a, b)).
proof: Proof. move=> ? Hp k. suff: forall m, steps k (p, (a, m + 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 + b' = (m + b' - b) + b by lia. by apply: IH. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun