proposition: Lemma compf_id_right m: correspondence m -> m \co (identity (source m)) = m.
proof: Proof. move=> cm. suff: ((graph m) \cg (identity_g (source m))= graph m). by rewrite /compose identity_graph0; aw => ->; apply: corresp_recov1. rewrite -diagonal_is_identity. set_extens t. by move /compg_P => [ {3} <- [y /diagonal_pi_P [pa ->] p1]]. have gm: (sgraph (graph m)) by fprops. move => tg; apply/compg_P; split; first by apply: (gm _ tg). move /setX_P: (proj2 cm _ tg) => [pt qt _]. by exists (P t); [ apply/diagonal_pi_P | rewrite pt ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)