proposition: Lemma iters_ind C F : (forall x, C x -> F x x) -> Transitive F -> (forall x y, iter R x y -> C x -> C y) -> (forall x y, R x y -> C x -> F x y) -> forall x y, iter R x y -> C x -> F x y.
proof: Proof. move=>H1 H2 H3 H x y; apply: iterf_ind x y=>// x y. by move=>H4 H5; split; [apply: H3 (iter1 H4) H5 | apply: H H5]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)