proposition: Lemma reaches_plus_reaches {x y z} : reaches_plus x y -> reaches y z -> reaches_plus x z.
proof: Proof. move=> [k [? Hk]] [k' Hk']. exists (k+k'). split; first by lia. by rewrite (steps_plus Hk). Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun