proposition: Lemma diagonal_graph_on x: graph_on (restricted_eq x) x = diagonal x.
proof: Proof. set_extens t. move /Zo_P => [pa [pb pc]]; apply /diagonal_i_P;split=> //. by move /setX_P: pa =>[]. move /diagonal_i_P=> [pa pb pc];apply/Zo_i => //; apply /setX_P; split => //;ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)