proposition: Theorem makeTrans_rightTrans : forall s s', makeTrans s s' <-> rightTrans s s'.
proof: Proof. intros. etransitivity. apply makeTrans_leftTrans. apply leftTrans_rightTrans. Qed.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid