proposition: Lemma sym_right_Transitive : right_Transitive.
proof: Proof. by move=> x y Rxy z; rewrite !(symR z); apply: sym_left_Transitive. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)