proposition: Lemma diag_app_fi a: injection (diagonal_application a).
proof: Proof. rewrite /diagonal_application/coarse; apply: lf_injective. by move=> y /=; fprops. by move => u v _ _; apply: pr1_def. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)