proposition: Lemma left_inverse_composable f f' r r': f' \coP f -> is_left_inverse f' r' -> is_left_inverse f r -> r \coP r'.
proof: Proof. move=> [_ _ c] li1 [[fr _ r1] _]. move: (left_i_target li1)=> r2. move: li1=> [[fr' _] _ _]. by split => //; rewrite r1 - c r2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)