The Coq mailing list

[CHAUVIN Barnabe <barnabe.chauvin AT gmail.com>]

Hello club !

I'm trying to simplify an hypothesis which contains something like this [a + - a = _] over Z (Let's call this hypothesis H).
So I thought it would be good to use the Zegal_left to do it, but Zegal_left do it the other way .. (i.e. It prove that [forall n m : Z, n = m -> n + - m = 0])

If H was a (sub)goal, I could have used the [cut] tactic, and it would have generated the [a=a] subgoal.
But because it's an hypothesis, I cannot use this tactic ..
I guess there is an easy workaround to do such a simplification in hypothesis ?

By the way, is-it possible, to directly rewrite this hypothesis ? Now, assume the hypothesis is of the form [0 = x0 * (x1 * a) + - a] (still over Z).
How can simplify it like [0=a * (x0 * x1 - 1)] ?  (And how can I simplify it if it was a goal ?)

I take this email to ask one little question that has no relation to the original subject.
What is the best to do a case disjunction on the value of a term during a proof ?
For example, if there is the term z:Z in the current goal, how do I create two subgoals with the hypothesis z=0 and z<>0 ?
Someone answered me on IRC to use the {}+{} types (sorry, I don't remember his name ..). It works very well, but I still have to prove the disjunction. So here is the extra question, how do I prove this :

   Lemma Z_0_or_not : forall z:Z, {z=0} + {z<>0}.

Thanks in advance !