Several useful lemmas about dom_rel and codom_rel.
Also I moved morphisms lemmas about dom_rel and codom_rel from HahnDom.v to other morphisms lemmas in HahnEquational.v.
This is because some of the new lemmas in HahnDom.v can be proved easily
given that morphism lemmas are already established.
Several useful lemmas about
dom_relandcodom_rel.Also I moved morphisms lemmas about
dom_relandcodom_relfromHahnDom.vto other morphisms lemmas inHahnEquational.v. This is because some of the new lemmas inHahnDom.vcan be proved easily given that morphism lemmas are already established.