proposition: Lemma compf_id_left m: correspondence m -> (identity (target m)) \co m = m.
proof: Proof. move=> cm. suff : ((identity_g (target m)) \cg (graph 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 p1 /diagonal_pi_P [_ <-]]]. 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 (Q t); [ rewrite pt | apply/diagonal_pi_P]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)