proposition: Lemma seq_singl_max_rt r a b (MAX: max_elt r b) : singl_rel a b ⨾ r＊ ≡ singl_rel a b.
proof: Proof. rewrite rtE; relsf; rewrite seq_singl_max_t; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid