proposition: Lemma strict_order_strict : forall A (R:binary A), order R -> strict_order (strict R).
proof: Proof. Proof using. introv [Re As Tr]. unfold strict. constructor; intros_all; simpls. destruct* H. applys* antisym_inv x y. split. applys* As. intros E. subst. applys* antisym_inv y z. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)