proposition: Corollary fcomp_identity_left E: {when (fun x => function x /\ (target x) = E), left_id (identity E) compose}.
proof: Proof. move => x [cx <-]; exact:compf_id_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)