proposition: Lemma diagonal_graph_P E I x: inc x (diagonal_graphp E I) <-> [/\ constantgp x, domain x = I & sub (range x) E].
proof: Proof. split; first by move /Zo_P => [] /gfunctions_P2 [pa pb pc] pd. move => [pa pb pc]; apply/Zo_i => //; apply/gfunctions_P2; split => //. by move: pa => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)