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