Bug#801484: ITP: coq-areamethod -- coq library for the area method decision procedure

[Riley Baird <BM-2cVqnDuYbAU5do2DfJTrN7ZbAJ246S4XiX@bitmessage.ch>]

Package: wnpp
Severity: wishlist
Owner: Riley Baird <BM-2cVqnDuYbAU5do2DfJTrN7ZbAJ246S4XiX@bitmessage.ch>

* Package name    : coq-areamethod
  Version         : 8.4+20150823
  Upstream Author : Julien Narboux <narboux@unistra.fr>
* URL             : http://dpt-info.u-strasbg.fr/~narboux/area_method.html
* License         : GPL-2+
  Programming Lang: Coq
  Description     : coq library for the area method decision procedure

This library is a coq implementation of the Area Method
decision procedure described by Shang-Ching Chou,
Xiao-Shan Gao and Jing-Zhong Zhang in their 1994 book
"Machine Proofs in Geometry".

This package contains more than 100 example theorems
which can be proved using the area method, such as:

-Ceva 
-Desargues
-Menelaus
-Pappus
-Pascal's axiom
-Gauss line
-Nine points circle
-Euler line