proposition: Lemma transp_seq_eqv_max_rt r : (r⁻¹)＊ ⨾ ⦗max_elt r⦘ ≡ ⦗max_elt r⦘.
proof: Proof. rewrite rtE; relsf; rewrite transp_seq_eqv_max_t; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid