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