let a, b be non zero Integer; :: thesis: ( Parity (a + b) = Parity b iff Parity a > Parity b )
thus ( Parity (a + b) = Parity b implies Parity a > Parity b ) :: thesis: ( Parity a > Parity b implies Parity (a + b) = Parity b )

proof

assume A1: Parity (a + b) = Parity b ; :: thesis: Parity a > Parity b
then A2: (Parity (a + b)) + 0 < (Parity a) + (Parity b) by XREAL_1:6;

per cases ( Parity a = Parity b or Parity b > Parity a or Parity b < Parity a ) by XXREAL_0:1;

suppose Parity a = Parity b ; :: thesis: Parity a > Parity b

hence Parity a > Parity b by A1, A2, Def1, PEQ; :: thesis: verum

end;

suppose Parity b > Parity a ; :: thesis: Parity a > Parity b

hence Parity a > Parity b by A1, PAP; :: thesis: verum

end;

suppose Parity b < Parity a ; :: thesis: Parity a > Parity b

hence Parity a > Parity b ; :: thesis: verum

end;

end;

end;

thus ( Parity a > Parity b implies Parity (a + b) = Parity b ) by PAP; :: thesis: verum