proposition: Lemma total_order_rclosure : forall A (R:binary A), total_order R -> total_order (rclosure R).
proof: Proof. Proof using. hint total_rclosure, order_rclosure. introv [Or To]. constructor~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)