left_cancel_semigroup.contravariant_mul_le_of_contravariant_mul_lt source