proposition: Lemma invertible_impl_bijective: forall {X Y:Type} (f:X->Y), invertible f -> bijective f.
proof: Proof. intros. destruct H. split. red; intros. congruence. red; intro. exists (g y). apply H0. Qed.
imports: Image Description FunctionalExtensionality