proposition: Lemma strict_total_order_of_total_order : forall A (R:binary A), total_order R -> strict_total_order (strict R).
proof: Proof. Proof using. introv [[Re Tr As] To]. constructor. apply~ trans_strict. intros x y. tests: (x = y). subst. apply trichotomy_eq. unfolds* strict. unfold strict. destruct (To x y). apply* trichotomy_left. apply* trichotomy_right. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)