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