proposition: Lemma infinite_increasing_power_bound0 X: fgraph X -> cardinal_fam X -> cprod X <=c (\csup (range X)) ^c (cardinal (domain X)).
proof: Proof. move => fX hb . rewrite cpowcr - cprod_of_same /cst_graph; apply: cprod_increasing; aww. move => x idx;rewrite LgV //. apply: card_sup_ub. move => t tx; move: tx => /(range_gP fX) [z zi ->]; apply: (hb _ zi). apply: (inc_V_range fX idx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)