proposition: Lemma inverse_bijective : forall (a b : E) (f g : E1), are_inverse a b f g -> bijective a b f.
proof: Proof. ir. unfold bijective in |- *. unfold are_inverse in H. xd. unfold surjective in |- *; xd. unfold covers in |- *. ir. apply ex_intro with (g x). xd. unfold injective in |- *; xd. unfold injects in |- *; ir. rewrite <- H1. rewrite <- H5. rewrite H1; au. am. Qed.
imports: set_theory