proposition: Lemma rtc_sub (h : seq nat) (R1 R2 : rel nat) x y : (forall x y, R2 x y -> (x \in h) && (y \in h)) -> (forall x y, R1 x y -> R2 x y) -> rtc h R1 x y -> rtc h R2 x y.
proof: Proof. move=>Rcond Rsub. have X : forall x y, R2 x y -> (x \in h) = (y \in h). - by move=>?? /Rcond /andP [->->]. case/rtcP=>[?? /Rsub/X //|Dx H]; apply/rtcP=>//. by split=>//; apply: iter_sub Rsub H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)