proposition: Lemma diagonal_class x u: inc u x -> class (diagonal x) u = singleton u.
proof: Proof. have h:= (proj1 (diagonal_equivalence x)). move=> ux; apply: set1_pr; first by apply/(class_P h) /diagonal_pi_P. by move => z /(class_P h) /diagonal_pi_P [_ ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)