let a, b be Integer; :: thesis: parity (a + b) = parity (a - b)
parity (a + b) = parity ((parity a) + (parity b)) by NAT_D:66
.= parity ((parity a) + (parity (- b))) by P1
.= parity (a + (- b)) by NAT_D:66 ;
hence parity (a + b) = parity (a - b) ; :: thesis: verum