proposition: Lemma seq_eqv_max_r r : ⦗max_elt r⦘ ⨾ r^? ≡ ⦗max_elt r⦘.
proof: Proof. rewrite crE; relsf; rewrite seq_eqv_max; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid