proposition: Lemma bijective_inverse : forall u : E, bijective u -> are_inverse u (inverse u).
proof: Proof. ir. unfold bijective in H; xe. pose (surjective_composable_left H0). pose (surjective_composable_right H0). pose (surjective_inverse_right H0). unfold are_inverse in |- *; ee. am. am. unfold composable in (type of c); ee. rewrite H3. ap e. apply injective_compose_with with u. ap compose_strong_axioms; au. ap identity_strong_axioms. am. unfold composable in |- *. ee. unfold injective in H; xe. ap compose_axioms; au. rewrite target_compose. unfold composable in (type of c0); xe. unfold composable in |- *; ee. unfold injective in H; xe. ap identity_axioms. rewrite target_identity; tv. rewrite <- associativity. rewrite e. ap extens. ap compose_strong_axioms. unfold composable in |- *; ee. ap identity_axioms. unfold injective in H; xe. rewrite source_identity. tv. ap compose_strong_axioms. unfold composable in |- *; ee. unfold injective in H; xe. ap identity_axioms. rewrite target_identity; tv. rewrite source_compose. rewrite source_compose. rewrite source_identity; tv. repeat rewrite target_compose. rewrite target_identity. tv. ir. repeat rewrite ev_compose. repeat rewrite ev_identity. tv. rewrite source_compose in H2. rewrite source_identity in H2; am. unfold injective in H; ee. unfold axioms in H. unfold property in H; xe. ap H. rewrite source_compose in H2. rewrite source_identity in H2. am. rewrite source_compose in H2; am. rewrite source_compose in H2. rewrite source_identity in H2. am. am. am. Qed.
imports: Arith functions