proposition: Lemma min_elt_restr_eq B (f: A -> B) : min_elt r a -> min_elt (restr_eq_rel f r) a.
proof: Proof. unfold restr_eq_rel in *; red; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid