proposition: Lemma max_elt_t : max_elt r a -> max_elt (r⁺) a.
proof: Proof. red; ins; apply clos_trans_t1n in REL; induction REL; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid