proposition: Lemma reaches_reaches_plus {x y z} : reaches x y -> reaches_plus 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