proposition: Lemma pres_iters_ind P Q F : preserved P R -> (forall x, P x -> Q x -> F x x) -> Transitive F -> (forall x y, iter R x y -> P x -> Q x -> Q y) -> (forall x y, R x y -> P x -> Q x -> F x y) -> forall x y, iter R x y -> P x -> Q x -> F x y.
proof: Proof. move=>pres H1 H2 H3 H4 x y O X1 X2; move: x y {X1 X2} O (conj X1 X2). apply: iterf_ind=>//; first by move=>s []; apply: H1. by move=>x y O [X Y]; move: (H3 _ _ (iter1 O) X Y) (H4 _ _ O X Y) (pres _ _ O X). Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)