proposition: Lemma surjective_composable_right : forall u : E, surjective u -> composable u (inverse u).
proof: Proof. ir. unfold composable in |- *; xe. unfold surjective in H; xe. ap axioms_from_strong. ap surjective_inverse_axioms; au. unfold inverse in |- *; rewrite target_create; tv. Qed.
imports: Arith functions