/usr/share/why/coq/WhyInt.v is in why 2.30+dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 | (*
* The Why certification tool
* Copyright (C) 2002 Jean-Christophe FILLIATRE
*
* This software is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public
* License version 2, as published by the Free Software Foundation.
*
* This software is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
*
* See the GNU General Public License version 2 for more details
* (enclosed in the file GPL).
*)
(* $Id: WhyInt.v,v 1.7 2006-11-02 09:18:20 hubert Exp $ *)
Require Export ZArith.
Require Export ZArith_dec.
Require Export Zdiv.
Theorem Znotzero : forall x:Z, {x <> 0%Z} + {x = 0%Z}.
Proof.
intro x.
elim (Z_eq_dec x 0); auto.
Qed.
|