proposition: Lemma pc_axiom0 c (g:= ((triple (domain c) (range c) c)) \co u): inc c (productb f) -> [/\ function g, c \cg (graph u) = graph g & (forall i, inc i (source u) -> Vg (graph g) i = Vg c (Vg (graph u) i))].
proof: Proof. move=> /setXb_P [fc dc eq]. have fu: function u by fct_tac. have cg: (c \cg (graph u) = graph g) by rewrite/g /compose; aw. have fg: function g. by rewrite/g; fct_tac; [ apply: function_pr; fprops| aw; ue]. split=>//. move=> i iu; rewrite ! corresp_g. have id: inc i (domain (c \cg graph u)). rewrite cg /g; fprops. by rewrite domain_fg //; aw. have fgc: fgraph (c \cg graph u) by ue. have fgv: fgraph (graph u) by fprops. move/(compg_pP):(fdomain_pr1 fgc id) => [y Jv Ju]. by move:(pr2_V fgv Jv)(pr2_V fc Ju); aw => <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)