proposition: Lemma fct_co_simpl_left f1 f2 g: g \coP f1 -> g \coP f2 -> bijection g ->g \co f1 = g \co f2 -> f1 = f2.
proof: Proof. move=> h1 h2 h3 h4. set g1:= inverse_fun g. have aux1: g1 \coP g by apply: composable_inv_f. move : (f_equal (fun z => g1 \co z) h4). rewrite (compfA aux1 h1) (compfA aux1 h2) bij_left_inverse //. move: h1 h2 => [pa pb pc] [pd pe pf]. rewrite {1} pc pf compf_id_l // compf_id_l //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)