proposition: Lemma cst_graph_pr x y: productb (cst_graph x y) = gfunctions x y.
proof: Proof. have xd: x = domain (cst_graph x y) by aw. by rewrite xd - setXb_eq_gfunctions - xd // => i ix; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)