proposition: Lemma bijective_inverse : forall (a b : E) (f : E1), bijective a b f -> are_inverse a b f (inverse a f).
proof: Proof. ir. unfold are_inverse in |- *; xd. unfold bijective in H; xd. ap surjective_inverse_axioms. unfold bijective in H; xd. ir. unfold bijective in H; ee. unfold injective in H2. ee. assert (axioms b a (inverse a f)). ap surjective_inverse_axioms; au. unfold axioms in H4. ap H3. ap H4. ap H. am. am. pose surjective_inverse_right. assert (inc (f x) b). ap H; am. pose (e _ _ _ _ H1 H5). am. ir. unfold bijective in H; xd. apply surjective_inverse_right with b. am. am. Qed.
imports: set_theory