proposition: Lemma seq_wmin_r_singl r a b (MAX: wmin_elt r a) : r ^? ⨾ singl_rel a b ≡ singl_rel a b.
proof: Proof. rewrite crE; split; relsf; rewrite seq_wmin_singl; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid