Theory Rank_Nullity_Theorem.Dual_Order
section "Dual Order"
theory Dual_Order
imports Main
begin
subsection‹Interpretation of dual wellorder based on wellorder›
lemma wf_wellorderI2:
assumes wf: "wf {(x::'a::ord, y). y < x}"
assumes lin: "class.linorder (λ(x::'a) y::'a. y ≤ x) (λ(x::'a) y::'a. y < x)"
shows "class.wellorder (λ(x::'a) y::'a. y ≤ x) (λ(x::'a) y::'a. y < x)"
using lin unfolding class.wellorder_def apply (rule conjI)
apply (rule class.wellorder_axioms.intro) by (blast intro: wf_induct_rule [OF wf])
lemma (in preorder) tranclp_less': "(>)⇧+⇧+ = (>)"
by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)