proposition: Lemma Exercise1_6h f: nonempty E -> nonempty F -> increasing_fun f (order_product2 r r') r'' -> ( (domain (source f)) = E /\ (range (source f)) = F).
proof: Proof. move=> ne1 ne2 [_ _ [_ sf _ ] _]. move: sf; rewrite order_product2_sr//. by move ->; rewrite (setX_domain _ ne2)(setX_range _ ne1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)