proposition: Lemma strict_total_order_asym : forall A (R:binary A), strict_total_order R -> asym R.
proof: Proof. Proof using. introv [Tr Tk]. intros x y. lets: (Tk x y). inverts~ H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)