proposition: Theorem left_inverse_compose f f' r r': f' \coP f -> is_left_inverse f' r' -> is_left_inverse f r -> is_left_inverse (f' \co f) (r \co r') .
proof: Proof. move=> c1 li1 li2. have cc:= left_inverse_composable c1 li1 li2. have tr'sr':= left_i_target li1. have sf'sr: (source f' = source r) by rewrite (proj33 cc). have sr'tf':= left_i_source li1. have [crf' crfi'] := li1. have [crf crfi] := li2. split. by split; [ fct_tac | fct_tac | aw;rewrite sr'tf']. have crrf: (r \co r') \coP f' by split; [ fct_tac | fct_tac| aw ]. rewrite compfA //- (@compfA r r' f') //. rewrite crfi' sf'sr compf_id_r ?crfi; aw; trivial;fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)