proposition: Lemma bijective_from_compose g f: g \coP f -> f \coP g -> g \co f = identity (source f) -> f \co g = identity (source g) -> [/\ bijection f, bijection g & g = inverse_fun f].
proof: Proof. move=> cgf cfg cgfi cfgi. move: (cfg) (cgf)=> [ff fg seq] [_ _ teq]. have injf: injection f by apply: inj_if_exists_left_inv; exists g. have injg: injection g by apply: inj_if_exists_left_inv; exists f. have bf: (bijection f). by split =>//; apply: surj_if_exists_right_inv; exists g; hnf; rewrite -teq. split=>//. by split=>//; apply: surj_if_exists_right_inv; exists f; hnf; rewrite - seq. have fif:= (bijective_inv_f bf). apply: function_exten; aw => // => x xs. have {2} -> : (x = Vf f (Vf g x)). by rewrite - compfV=>//;rewrite cfgi idV =>//. rewrite (inverse_V2 bf) // seq; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)