proposition: Lemma set_equiv_max_elt (S: r ≡ r') : max_elt r ≡₁ max_elt r'.
proof: Proof. unfold max_elt, same_relation, set_equiv, set_subset in *; intuition; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid