proposition: Lemma Transitive_sumR : Transitive R1 -> Transitive R2 -> Transitive sumR.
proof: Proof. by move=>t1 t2; case=>x; case=>y; case=>z //; [apply:t1 | apply:t2]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)