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