proposition: Lemma obind_oiter {X : Type} (f : X -> option X) k x : obind f (Nat.iter k (obind f) (Some x)) = Nat.iter k (obind f) (f x).
proof: Proof. elim: k; [done|by move=> k /= ->]. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun