proposition: Lemma card_sup_image E f g: (forall x, inc x E -> f x <=c g x) -> \csup (fun_image E f) <=c \csup (fun_image E g).
proof: Proof. move => h. have pb: cardinal_set (fun_image E g). by move => t /funI_P [z zE ->]; case: (h _ zE). apply: card_ub_sup => //; first by apply: CS_sup. move=> i /funI_P [z zE ->]; apply: (cleT (h _ zE)). apply: card_sup_ub => //; apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)