proposition: Lemma Equivalence_sumR : Equivalence_rel R1 -> Equivalence_rel R2 -> Equivalence_rel sumR.
proof: Proof. case/Equivalence_relS=>r1 s1 t1 /Equivalence_relS [r2 s2 t2]. apply/Equivalence_relS; split. - by apply: Reflexive_sumR. - by apply: Symmetric_sumR. by apply: Transitive_sumR. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)