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