proposition: Lemma iters_ind' C F : (forall x, C x -> F x x) -> (forall x y z, C x -> C y -> C z -> F x y -> F y z -> F x z) -> (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 H4 x y [n]; elim: n x=>[|n IH] x. - by move=>->; apply: H1. case=>z [O] H Cx; move: (H3 _ _ (iter1 O) Cx)=>Cz. by apply: H2 (IH _ H Cz)=>//; [apply: H3 Cz; exists n | apply: H4]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)