Theorem Function.Injective.surjective_comp_right

Modification history