proposition: Lemma iterb_ind C F : (forall x, C x -> F x x) -> Transitive F -> (forall x y, R x y -> C y -> C x /\ F x y) -> forall x y, iter R x y -> C y -> F x y.
proof: Proof. move=>X Y H x y [n]; elim: n x y=>[|n IH] x y; first by move=>->; apply: X. by case/iterS=>z[]{}/IH Z O /(H _ _ O) [/Z]; apply: Y. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)