Proof of convex hull correctness in Coq

Name		Name	Last commit message	Last commit date
Latest commit History 19 Commits
Compiler		Compiler
Convex Hull		Convex Hull
.gitattributes		.gitattributes
CoInductive.v		CoInductive.v
ConvexHull-old.v		ConvexHull-old.v
CpdtTactics.v		CpdtTactics.v
Geometry of plain.v		Geometry of plain.v
Geometry.v		Geometry.v
Hypermap.v		Hypermap.v
Mechanical theorem prover in CG.pdf		Mechanical theorem prover in CG.pdf
PointBox.v		PointBox.v
Poset.v		Poset.v
README.md		README.md
SfLib.v		SfLib.v
SortedList.v		SortedList.v
Sorting.v		Sorting.v
lists_exce.v		lists_exce.v
natural numbers.v		natural numbers.v

Provide feedback