proposition: Theorem exists_right_composable_unique f g h h': function f -> injection g -> target f = target g -> g \coP h -> g \coP h' -> g \co h = f -> g \co h' = f -> h = h'.
proof: Proof. move=> ff [_ ig] tftg cgh cgh' cghf cghf'. move: (cgh)(cgh') => [p1 p2 p3] [_ p5 p6]. rewrite -cghf' in cghf. have shh': source h = source h' by rewrite -(compf_s h g) -(compf_s h' g) cghf. apply: function_exten => //; [ ue | move=> x xsh;apply: ig ]. + by rewrite p3; Wtac. + rewrite p6; Wtac; ue. + move: (f_equal (Vf ^~ x) cghf); rewrite !compfV //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)