proposition: Lemma order_rclosure_of_strict_order : forall A (R:binary A), strict_order R -> order (rclosure R).
proof: Proof. Proof using. introv [Re As Tr]. rewrite rclosure_eq_fun. constructor; simpl. intros_all~. introv [H1|E1] [H2|E2]; subst; auto. left. apply* trans_inv. introv [H1|E1] [H2|E2]; try subst; auto. false. apply* As. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)