proposition: Lemma power_cofinality x: \2c <=c x -> x <c x ^c (cofinality_c x).
proof: Proof. move=> x1; move: (cofinality_c_rw x1) => [pb pc _]. move: pc => [f [[pc pd] pe pf]]. set g := cst_graph (domain f) x. have pg: fgraph g by rewrite /g/cst_graph; fprops. have ph: domain f = domain g by rewrite /g/cst_graph; aw. have pi: (forall i, inc i (domain f) -> (Vg f i) <c (Vg g i)). by move=> i idf; rewrite /g/cst_graph LgV//;apply:pd. by move: (compare_sum_prod pc pg ph pi); rewrite [cprod g] cprod_of_same pe pf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)