proposition: Lemma diagonal_i_P x u: inc u (diagonal x) <-> [/\ pairp u, inc (P u) x & P u = Q u].
proof: Proof. split; first by case/Zo_P => /setX_P [ta tb _] tc. move=> [ta tb tc]; apply: Zo_i => //;rewrite -ta; apply: setXp_i => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)