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