proposition: Lemma bijective_double_inverseC1 (a b:Set) (f:a->b) g g' (Ha: g \o f =1 @id a)(Hb: f \o g' =1 @id b) (h := inverseC (bijective_double_inverseC Ha Hb)): g =1 h /\ g' =1 h.
proof: Proof. have sg: (g' =1 g). by move=> x; rewrite -{1} (Ha (g' x)) -{2} (Hb x) !composeC_ev. suff gh: (g' =1 h) by split =>//; apply: ftrans gh. by move => x; rewrite /h - {2} (Hb x) inverseC_pra. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)