proposition: Lemma min_elt_seq1 : min_elt r' a -> min_elt (r ⨾ r') a.
proof: Proof. unfold seq; red; ins; desf; apply H in REL0; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid