proposition: Lemma reaches_non_terminating' {x y} : reaches x y -> non_terminating x -> non_terminating y.
proof: Proof. move=> [k' Hk'] Hx k Hk. apply: (Hx (k' + k)). by rewrite (steps_plus Hk'). Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun