, le_S : (n,m:nat)(le n m) -> (le n (S m))

, Axiom monoticity : (n,m:nat)(le n m) -> (le (f n) (f m))

, Lemma le_x_Sx : (x:nat)(le x (S x))

, Theorem L1 : (a:nat)

, At last, let us show some examples on which the tactic fails

, Error: Not provable in DPC, vol.2

-. Error,

G. Bellin and J. Ketonen, A decision procedure revisited : Notes on direct logic, linear logic and its implementation, Theoretical Computer Science, vol.95, pp.115-142, 1992.

C. Cornes, J. Courant, J. Filli^-atre, G. Huet, P. Manoury et al., The Coq Proof Assistant Reference Manual Version 5, INRIA, vol.10, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00069994

J. Gallier, Constructive Logics. Part I: A Tutorial on Proof Systems and Typed {Calculi, Digital Equipment Corporation, vol.8, 1991.

J. Gallier, Constructive Logics. Part II: Linear Logic and Proof Nets, Digital Equipment Corporation, vol.8, 1991.

J. Girard, Y. Lafont, and P. , Proofs and Types. C a m bridge Tracts in Theoretical Computer Science 7, 1989.

J. Ketonen and R. Weyhrauch, A decidable fragment of Predicate Calculus, Theoretical Computer Science, vol.32, pp.297-307, 1984.

R. Lalement, Etudes et recherches en Informatique, 1990.

X. Leroy and P. Eis, Manuel de r ef erence du langage Caml. I n terEditions, 1993.

P. D. Lincoln and N. Shankar, Proof search in rst-order linear logic and other cut-free sequent calculi, Symposium on Logic in Computer Science, 1994.

A. Martelli and U. Montanari, An eecient uniication algorithm, ACM Trans. Prog. Lang. Syst, vol.4, issue.2, pp.258-282, 1982.

P. Eis and X. Leroy, Le langage Caml. I n terEditions, 1993.