proposition: Lemma total_order_intro : forall A (R:binary A), trans R -> antisym R -> total R -> total_order R.
proof: Proof. Proof using. introv Tra Ant Tot. constructor~. constructor~. intros_all. destruct~ (Tot x x). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)