proposition: Lemma strict_order_inverse : forall A (R:binary A), strict_order R -> strict_order (inverse R).
proof: Proof. Proof using. hint antisym_inverse, trans_inverse, asym_inverse. introv [Ir As Tr]. constructor~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)