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