proposition: Lemma total_preorder_rclosure : forall A (R:binary A), total_preorder R -> total_preorder (rclosure R).
proof: Proof. Proof using. hint trans_rclosure, total_rclosure. introv [Re Tr]. constructor~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)