Module ...lib.coq.WhyInt

Require Export ZArith.
Require Export ZArith_dec.
Require Export Zdiv.

Theorem Znotzero : (x:Z){`x<>0`}+{`x=0`}.
Proof.
Intro x. Elim (Z_eq_dec x `0`) ; Auto.
Save.

Index
This page has been generated by coqdoc