How to Install and Uninstall coq-highschoolgeometry Package on Ubuntu 16.04 LTS (Xenial Xerus)

Last updated: November 22,2024

1. Install "coq-highschoolgeometry" package

Here is a brief guide to show you how to install coq-highschoolgeometry on Ubuntu 16.04 LTS (Xenial Xerus)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                coq-highschoolgeometry
            
                    
    
    Copied

2. Uninstall "coq-highschoolgeometry" package

Please follow the instructions below to uninstall coq-highschoolgeometry on Ubuntu 16.04 LTS (Xenial Xerus):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                coq-highschoolgeometry
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the coq-highschoolgeometry package on Ubuntu 16.04 LTS (Xenial Xerus)

Package: coq-highschoolgeometry
Priority: optional
Section: universe/math
Installed-Size: 4296
Maintainer: Ubuntu Developers
Original-Maintainer: Riley Baird
Architecture: all
Version: 8.4+20150620-1
Depends: coq
Filename: pool/universe/c/coq-highschoolgeometry/coq-highschoolgeometry_8.4+20150620-1_all.deb
Size: 1473866
MD5sum: 3e23577ddaf5b6611b8727597ddf34cf
SHA1: b6962bfecd3eba6b43f2f205894cd16f5cc5a8d2
SHA256: 0d2a5252b46533daf3b74fe1acbdd77fa444d0e3edce9a47395aa587066b30b9
Description-en: coq library for high school geometry proofs/formalisation
Created by Frédérique Guilhot, this library consists of a collection of
"chapters" spanning most of the geometry taught in French high schools.
.
The first part "2-3 dimensional affine geometry" deals with formalising:
points, vectors, barycenters, oriented lengths
collinearity, coplanarity
parallelism and incidence of straight lines
proofs of Thales and Desargues theorems.
.
In the second part "3 dimensional affine geometry", theorems about these
things are proven:
relative positions of two straight lines in the space
relative positions of a straight line and a plane
relative positions of two planes
parallelism and incidence properties for several planes and straight lines
.
The third part "2-3 dimensional euclidean geometry" deals with formalising:
scalar product, orthogonal vectors, and unitary vectors
Euclidean distance and orthogonal projection on a line
proofs of Pythagorean theorem, median theorem
.
The fourth part "space orthogonality" deals with formalising:
orthogonal line and plan
.
The fifth part "plane euclidean geometry" deals with formalising:
affine coordinate system, orthogonal coordinate system, affine coordinates
oriented angles
trigonometry
proofs of Pythagorean theorem, median theorem, Al-Kashi and sine theorems
perpendicular bisector, isocel triangle, orthocenter
circle, cocyclicity, tangency (line or circle tangent)
signed area, determinant
equations for straight lines and circles in plane geometry
.
The sixth part "plane transformations", deals with formalising:
translations, homothety
rotations, reflexions
composition of these transformations.
conservation of tangency for these transformations.
.
In the seventh part "applications", these are proven:
Miquel's theorem, orthocenter theorem, Simson line
circle power and plane inversion
Euler line theorem and nine point circle theorem
.
The eighth part "complex numbers", deals with formalising:
the field properties of complex numbers
application to geometry of complex numbers
Description-md5: 4df50d9e6a0033853f51ad710483a098
Homepage: http://www-sop.inria.fr/lemme/Frederique.Guilhot/geometrie.html
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Origin: Ubuntu