proposition: Theorem left_inv_compose_rf f f' r'': f' \coP f -> is_left_inverse (f' \co f) r'' -> is_left_inverse f (r'' \co f').
proof: Proof. move=> cff [[ aa bb]]; aw; move => crffi cc. have [ff' ff seq]: f' \coP f by []. have crf: r'' \coP f' by hnf. split; [saw; fct_tac | by rewrite - compfA ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)