theorem
proved
PRCPrimeCalibratedMixedPrimePairWitnessCharacter_same_or_distinct
show as:
PRCPrimeCalibratedMixedPrimePairWitnessCharacter_same_or_distinct