proposition: Lemma diagonal_pi_P x u v: inc (J u v) (diagonal x) <-> (inc u x /\ u = v).
proof: Proof. apply: (iff_trans (diagonal_i_P x (J u v))); aw. split; [by case | move => []; split; fprops ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)