proposition: Lemma surjective_inverse_right : forall u : E, surjective u -> compose u (inverse u) = identity (target u).
proof: Proof. ir. assert (axioms u). unfold surjective in H; xe. ap extens. ap compose_strong_axioms. ap surjective_composable_right. am. ap identity_strong_axioms. rewrite source_compose. rewrite source_identity. unfold inverse in |- *; rewrite source_create. tv. rewrite target_compose. rewrite target_identity; tv. ir. rewrite ev_compose. rewrite ev_identity. unfold inverse in |- *. rewrite ev_create. unfold surjective in H. xe. rewrite source_identity in H2. pose (Transformation.surjective_inverse_right H3 H2). ap e. rewrite source_identity in H2; am. rewrite source_identity in H2; am. rewrite source_compose in H1. am. Qed.
imports: Arith functions