proposition: Lemma pres_itercf_ind : preserved Pc Rc -> (forall a x, P a x -> Q a x -> F a x a x) -> Transitive Fc -> (forall a x b y, R a x b y -> P a x -> Q a x -> Q b y /\ F a x b y) -> forall a x b y, iterc R a x b y -> P a x -> Q a x -> F a x b y.
proof: Proof. move=>H1 H2 H3 H4 a x b y; apply: (@pres_iterf_ind _ Rc Pc Qc Fc)=>//. - by case=>a' x' [b' y']; apply: (H1 (a', x') (b', y')). - by case=>a' x'; apply: H2. by case=>a' x' [b' y']; apply: H4. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)