proposition: Lemma seq_wmin_rt_singl r a b (MAX: wmin_elt r a) : r ＊ ⨾ singl_rel a b ≡ singl_rel a b.
proof: Proof. rewrite rtE; split; relsf; rewrite seq_wmin_t_singl; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid