proposition: Lemma total_preorder_refl : forall A (le:binary A), total_preorder le -> refl le.
proof: Proof. Proof using. introv [Tr To]. intros x. destruct~ (To x x). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)