## Stream: Coq users

### Topic: From successor

#### sara lee (Jul 16 2022 at 17:09):

I need n > 0 to solve the goal statement, but in hypothesis i have (S n)> 0. In this case what i should do or what modification i should made in hypothesis ?

#### Mukesh Tiwari (Jul 16 2022 at 21:08):

You question does not have enough information to answer it precisely. Could you please post your theorem that you are trying to prove. Given that your goal demands `0 < n` and you have `0 < S n` in assumption, it is not provable because `n` can be `0` and your assumption holds but the goal is not provable (`0 < 0`).

#### sara lee (Jul 17 2022 at 08:27):

``````H0: (S n)>0
H: n>0 ->
(length l > 0->
z < length l ->
count z l <= count 0 l)
goal: count z l  <= S ( count 0 l)
``````

I have n>0 in hypothesis(initially) ,but after induction it became (S n). To prove above i need n>0 but have (S n).

#### James Wood (Jul 19 2022 at 12:55):

What does it look like before the induction? For the `n > 0` assumption to remain as-is in the type of `H` seems a bit strange.

#### sara lee (Jul 26 2022 at 14:04):

before induction it is n>0. I want to prove statement " if count of 0 is greater than count of z in l,then addition of another 0 will not effect the existing relation.

#### Pierre Castéran (Jul 26 2022 at 17:17):

Is it an induction on `n` ? But `n`does not occur in the right hand side of the implication, which depends only on `z`and `l`. If I try to prove some proposition `forall n, 0 < n -> Q`, I obtain a similar goal.
May be it's worth trying an induction on `l`. But it's difficult to be more specific without the exact Coq script which led to this problem.

#### sara lee (Jul 30 2022 at 06:20):

I have function f which is responsible for the addition of different elements in the output list after test condition.
Now have hypothesis that in the output list count of z is less or equal to 0. If test condition is satisfied and 0 is adding in the list
. Performed induction on l and destruct n (both). I want to know how i should proceed? Yes proving proposition.

Last updated: Jun 14 2024 at 19:02 UTC