proposition: Lemma total_order_le_is_rclosure_lt : forall (To:total_order R), le = rclosure lt.
proof: Proof. Proof using. extens. intros. total_order_normalize. iff M. tests~: (x = y). destruct M. autos*. subst*. dintuition eauto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)