proposition: Theorem wf_rightTrans : well_founded (rightTrans R).
proof: Proof. red. eapply Fix. eapply wf_R. clear. intros. constructor. intros. revert H. induction H0. { intros. eauto. } { intros. eapply IHrightTrans; clear IHrightTrans. specialize (H1 _ H). inversion H1. intros. eapply H2. eapply RTFin. eassumption. } Defined.
imports: ExtLib.Relations.TransitiveClosure