← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/success/Omega2.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/success/Omega2.v
 
1
Require Import ZArith Omega.
 
2
 
 
3
(* Submitted by Yegor Bryukhov (#922) *)
 
4
 
 
5
Open Scope Z_scope.
 
6
 
 
7
Lemma Test46 : 
 
8
forall v1 v2 v3 v4 v5 : Z,
 
9
((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
 
10
9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
 
11
((9 * v3) + (2 * v5)) + (5 * v2) = 3 * v4 ->
 
12
0 > 6 * v1 ->
 
13
(0 * v3) + (6 * v2) <> 2 ->
 
14
(0 * v3) + (5 * v5) <> ((4 * v2) + (8 * v2)) + (2 * v5) ->
 
15
7 * v3 > 5 * v5 ->
 
16
0 * v4 >= ((5 * v1) + (4 * v1)) + ((6 * v5) + (3 * v5)) ->
 
17
7 * v2 = ((3 * v2) + (6 * v5)) + (7 * v2) ->
 
18
0 * v3 > 7 * v1 ->
 
19
9 * v2 < 9 * v5 ->
 
20
(2 * v3) + (8 * v1) <= 5 * v4 ->
 
21
5 * v2 = ((5 * v1) + (0 * v5)) + (1 * v2) ->
 
22
0 * v5 <= 9 * v2 ->
 
23
((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
 
24
-> False.
 
25
intros.
 
26
omega.
 
27
Qed.
 
28