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