proposition: Lemma rev_Trans : Transitive R -> Transitive (fun x y => R y x).
proof: Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)