let a be odd Nat; :: thesis: for b being non trivial odd Nat holds
( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) )
let b be non trivial odd Nat; :: thesis: ( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) )

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

suppose A1: Parity (a + 1) = Parity (b - 1) ; :: thesis: ( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) )

then Parity ((a + 1) + (b - 1)) >= (Parity (a + 1)) + (Parity (b - 1)) by PEQ;
hence ( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) ) by A1; :: thesis: verum

end;

suppose B1: Parity (a + 1) > Parity (b - 1) ; :: thesis: ( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) )

then Parity ((a + 1) + (b - 1)) = Parity (b - 1) by PAP;
hence ( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) ) by B1, XXREAL_0:def 9; :: thesis: verum

end;

suppose B1: Parity (a + 1) < Parity (b - 1) ; :: thesis: ( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) )

then Parity ((a + 1) + (b - 1)) = Parity (a + 1) by PAP;
hence ( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) ) by B1, XXREAL_0:def 9; :: thesis: verum

end;

end;