replace lemma realpow_two_diff with new lemma square_diff_square_factored
theory Probabilityimports Complete_Measure Probability_Measure Infinite_Product_Measure Independent_Family Conditional_Probability Information "ex/Dining_Cryptographers" "ex/Koepf_Duermuth_Countermeasure"beginend