proposition: Lemma surjective_inverse_axioms : forall u : E, surjective u -> strong_axioms (inverse u).
proof: Proof. ir. unfold strong_axioms in |- *; xe. unfold inverse in |- *. ap create_axioms. unfold property in |- *. ap Transformation.surjective_inverse_axioms. unfold surjective in H; xe. unfold inverse in |- *. ap create_like. Qed.
imports: Arith functions