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