theorem
proved
PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_nonunit_coherent
show as:
PRCPrimeCalibrationForcesPrimeFloorSuccessorTransportTarget_of_nonunit_coherent