The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Greetings,

I'm trying to find the syntax for induction principle with some
conditions. I am searching book, Reference Manual and other literature but
I can not find it.

Concrete, for example, I need this axiom:

Axiom Test : forall P : nat -> Prop, P (x+n) -> P (x-n) -> P (x+2*n) -> P
(x-2*n) -> forall y : nat, P y.

Parameters x, y and n must have type nat. But, expressions (x+n), (x-n),
(x+2*n) and (x-2*n) must be greater of 0 and lesser than 100. When I elim
value y in proof using this axiom, only such values have to be introduced.

How can I write such induction principle?

Thank you very much,

Marko Malikoviæ