proposition: Lemma seq_max_rt r r' b (MAX: max_elt r' b) (COD: forall x y, r x y -> y = b) : r ⨾ r'＊ ≡ r.
proof: Proof. rewrite rtE; relsf; rewrite seq_max_t; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid