proposition: Lemma order_inverse : forall A (R:binary A), order R -> order (inverse R).
proof: Proof. Proof using. hint trans_inverse, antisym_inverse. introv [Re Tr An]. constructor~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)