proposition: Lemma seq_wmax r r' b (MAX: wmax_elt r' b) (COD: forall x y, r x y -> y = b) : r⨾ r' ⊆ r.
proof: Proof. unfold seq; red; ins; desf; eauto. specialize (COD _ _ H); desf; apply MAX in H0; desf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid