proposition: Theorem leftTrans_rightTrans : forall x y, leftTrans x y <-> rightTrans x y.
proof: Proof. split. { destruct 1. apply RTFin; assumption. eapply leftTrans_rightTrans_acc. eassumption. eapply RTFin. eassumption. } { destruct 1. apply LTFin. assumption. eapply rightTrans_leftTrans_acc. eassumption. eapply LTFin. eassumption. } Qed.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid