proposition: Lemma bijective_double_inverseC (a b:Set) (f:a->b) g g': g \o f =1 @id a -> f \o g' =1 @id b -> bijectiveC f.
proof: Proof. move=> c1 c2; split. move=> x x' /(congr1 g); rewrite -!(composeC_ev g f) !c1 //. move=> x; exists (g' x); rewrite -!(composeC_ev f g') c2 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)