proposition: Lemma ord_sup_2funI X f g: {inc X, f =1 g} -> \osup (fun_image X f) = \osup (fun_image X g).
proof: Proof. move=> h; congr union. set_extens t; move /funI_P => [z zX ->]; apply /funI_P;ex_tac. by symmetry; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)