proposition: Lemma steps_plus {k x k' y} : steps k x = Some y -> steps (k + k') x = steps k' y.
proof: Proof. by rewrite /steps Nat.add_comm /Nat.iter nat_rect_plus /= => ->. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun