proposition: Lemma steps_k_monotone {k x} k' : steps k x = None -> k <= k' -> steps k' x = None.
proof: Proof. move=> + ?. have ->: k' = (k' - k) + k by lia. elim: (k' - k); first done. by move=> ? IH /IH /= ->. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun