The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 15 Feb 2014 23:29:23 +0200,
Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 a écrit :

> Hi all,
> 
> Let's say I have `length tl = n - 1` as goal and `H: n <> 0`. Can I
> apply same constructor/function to both sides of the equation in goal?
> Like applying S and having:
> 
> > S (length tl) = S (n - 1)
> 
> Is this possible? If not, why?

It is possible, trivial and you do not even require H.
Here, "f_equal" would be enough (assert (S (length tl) = S (n-1)).
f_equal.). There are numerous other ways to do it.

> 
> Thanks!
> 
> 
> ---
> Ömer Sinan Ağacan
> http://osa1.net