proposition: Lemma canon_proj_diagonal_fb_contra r: equivalence r -> bijection (canon_proj r) -> r = diagonal (substrate r).
proof: Proof. move => pa pb. set_extens t; last first. by move /diagonal_i_P => [Px px qx]; rewrite -Px -qx; apply: reflexivity_e. move => tr; move: (pa) => [sa _ _ _]; move: (sa _ tr) => pt. have ptsr: inc (P t) (substrate r) by substr_tac. have qtsr: inc (Q t) (substrate r) by substr_tac. apply /diagonal_i_P; split => //. move: (bij_inj pb); rewrite canon_proj_s => h; move: (h _ _ ptsr qtsr). rewrite !canon_proj_V //. by apply; apply: class_eq1 => //;rewrite /related pt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)