proposition: Lemma iterc_ind : (forall a x b y, R a x b y -> C a x -> C b y) -> forall a x b y, iterc R a x b y -> C a x -> C b y.
proof: Proof. move=>H a x b y; apply: (@iter_ind _ Rc Cc)=>//. by case=>a' x' [b' y']; apply: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)