theorem
proved
canonicalRemainderLineDifferentiabilityNearZero_of_actionLineDifferentiabilityNearZero
show as:
canonicalRemainderLineDifferentiabilityNearZero_of_actionLineDifferentiabilityNearZero