proposition: Lemma min_transp : min_elt r⁻¹ ≡₁ max_elt r.
proof: Proof. split; unfold min_elt, max_elt, transp, set_subset; ins; desf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid