proposition: Lemma strict_total_order_inverse : forall A (R:binary A), strict_total_order R -> strict_total_order (inverse R).
proof: Proof. Proof using. introv [Tr Tk]. constructor. apply~ trans_inverse. apply~ trichotomous_inverse. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)