proposition: Lemma comp_is_id_then_bijective : forall (A B : Setoid) (f : MAP A B) (g : MAP B A), Equal (comp_map_map g f) (Id A) -> Equal (comp_map_map f g) (Id B) -> bijective f.
proof: Proof. intros A B f g H' H'0; try assumption. unfold bijective in |- *. split; [ try assumption | idtac ]. apply comp_injective with A g; auto with algebra. apply injective_comp with (f := Id A); auto with algebra. apply comp_surjective with B g; auto with algebra. apply surjective_comp with (f := Id B); auto with algebra. Qed.