The Coq mailing list

[Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>]

I'm trying to prove the following:

Goal forall x y:Z, (x <> 0) -> (y <> 0) -> (x+y = 0) -> 

   (~(Zabs x < Zabs y)) /\  (~(Zabs y < Zabs x)) /\ (Zabs x = Zabs y).

After typing in the following:

intros;induction x;induction y.

contradiction.

contradiction.

contradiction.

contradiction.

unfold Zabs.

split.

induction p;induction p0.

I end up with 14 subgoals on positives. But I don't quite understand

the notation p~1, what is ~?

Is there a possible proof without having to induct on p and p0?

Thanks

Ashish

14 subgoals

  

  p : positive

  p0 : positive

  H : Zpos p~1 <> 0

  H0 : Zpos p0~1 <> 0

  H1 : Zpos p~1 + Zpos p0~1 = 0

  IHp : Zpos p <> 0 -> Zpos p + Zpos p0~1 = 0 -> ~ Zpos p < Zpos p0~1

  IHp0 : Zpos p0 <> 0 ->

         Zpos p~1 + Zpos p0 = 0 ->

         (Zpos p <> 0 -> Zpos p + Zpos p0 = 0 -> ~ Zpos p < Zpos p0) ->

         ~ Zpos p~1 < Zpos p0

  ============================

   ~ Zpos p~1 < Zpos p0~1

....