proposition: Lemma seq_min_singl r a b (MAX: min_elt r a) : r ⨾ singl_rel a b ≡ ∅₂.
proof: Proof. unfold singl_rel, seq; split; red; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid