proposition: Lemma seq_rt_eqv_min r : r＊ ⨾ ⦗min_elt r⦘ ≡ ⦗min_elt r⦘.
proof: Proof. rewrite rtE; relsf; rewrite seq_t_eqv_min; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid