proposition: Lemma bijective_impl_invertible: forall {X Y:Type} (f:X->Y), bijective f -> invertible f.
proof: Proof. intros. destruct H. assert (forall y:Y, {x:X | f x = y}). intro. apply constructive_definite_description. pose proof (H0 y). destruct H1. exists x. red; split. assumption. intros. apply H. transitivity y. auto with *. auto with *. pose (g := fun y:Y => proj1_sig (X0 y)). pose proof (fun y:Y => proj2_sig (X0 y)). simpl in H1. exists g. intro. apply H. unfold g; rewrite H1. reflexivity. intro. unfold g; apply H1. Qed.
imports: Image Description FunctionalExtensionality