proposition: Lemma seq_wmin_rt r r' b (MAX: wmin_elt r b) (COD: forall x y, r' x y -> x = b) : r ＊⨾ r' ≡ r'.
proof: Proof. rewrite rtE; split; relsf; rewrite seq_wmin_t; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid