Add LICENSE

LICENSE

+NON-COMMERCIAL LICENSE AGREEMENT FOR NC-COQ SOFTWARE
+
+PREAMBLE
+
+NC-Coq permits formal proofs of network calculus and proposes examples
+using those results.
+
+NC-Coq is and remains property of ONERA (www.onera.fr) that solely
+holds the economic rights over it.
+
+ONERA distributed NC-Coq under the terms of a Non-Commercial License
+Agreement that grants the right to use the software for educational,
+academic research or test and evaluation purposes only, and prohibits
+any commercial use. Any use of the software, other than as authorised
+under this licence agreement is prohibited (to the extent such use is
+covered by a right of the copyright holder of the software).
+
+For commercial use, please contact the authors of the Software.
+
+DEFINITIONS
+
+* "Licensee" means the Software user having accepted the Agreement.
+
+* "Licensor" means ONERA
+
+* "Agreement" means this license agreement and it shall not be
+  modified or amended except by an instrument in writing signed by
+  both parties hereto.
+
+* "Software" means NC-COQ software in its Object Code and/or Source
+  Code form and, where applicable, its documentation.
+
+* "Derivative Work" means a work that is a modification of,
+  enhancement to, derived from, or based upon the Software.
+
+TERMS AND CONDITIONS
+
+1. Scope of rights granted
+
+On use and modification : Licensor hereby grants to the Licensee, who
+accepts, a revocable, non-exclusive, non-transferable, royalty-free
+and worldwide right to use the Software and prepare Derivative Works
+solely for educational, academic and non-commercial research
+endeavors, or test and evaluation purposes. Any other use is
+considered as commercial use and is prohibited. In particular,
+Licensee may not use the Software in connection with any activities
+which purpose is to procure a commercial gain to him or others.
+
+On distribution : The Licensee is authorized to distribute the
+Software or any Derivative Works of the Software only under the same
+terms and conditions as in this License, no other rights to the
+Software or Derivative Works that are different from those provided by
+this License can be granted. A copy of this Agreement must accompany
+the distribution of the Software or any derivative works of the
+Software.
+
+2. Acceptance, Duration and Termination
+
+The Licensee shall be deemed as having accepted the terms and
+conditions of this Agreement as soon as he will have access to the
+software and exercises any of the rights granted hereunder for the
+first time.
+
+The Agreement shall remain in force for the entire legal term of
+protection of the economic rights over the Software.
+
+The Agreement and the rights granted hereunder will terminate
+automatically upon any breach by the Licensee of the terms of the
+Agreement. Upon termination of this Agreement, Licensee shall
+immediately discontinue all use of the Software.
+
+Such a termination will not terminate the licence agreements of any
+person who has received the Software or any Derivative Works of the
+Software from the Licensee, provided such persons remain in full
+compliance with the Agreement.
+
+3. Publication Credit
+
+Licensee agrees to mention Licensor and the name of the Software with
+appropriate citations in any publication, presentation, document
+containing results obtained in whole or in part through the use of the
+Software.
+
+4. Disclaimer of Warranty
+
+The Software is a research and development Software, it is not an
+industrial Software and may therefore contain errors, 'bugs' or a lack
+of comments inherent to this type of development. For this reason, the
+Software is provided "AS IS" without warranties of any kind concerning
+the Software including, but not limited to, merchantability, fitness
+for a particular purpose, absence of defects or errors, accuracy,
+non-infringement of intellectual property rights.
+
+5. Disclaimer of Liability
+
+Licensor will in no event be liable for any direct or indirect,
+material or moral, damages of any kind, arising out of the Agreement
+or of the use of the Software, including, but not limited to, damages
+for loss of goodwill, work stoppage, computer failure or malfunction,
+loss of data or any commercial damage, even if the Licensor has been
+advised of the possibility of such damage.
+
+The Licensee uses the Software at its own risk and expense.
+
+6. Additional Services
+
+Support or issues updates to the software are not provided with the
+software and not included in the Agreement.
+
+7. Applicable law and settling of disputes
+
+This Agreement shall be governed and construed in accordance with
+French law.
+
+The Parties agree to attempt to settle amicably any controversy or
+claim arising under this Agreement or a breach of this
+Agreement. Thereafter, both parties agree that all disputes between
+them arising out of or relating to this Agreement, shall be submitted
+to non-binding mediation unless the parties mutually agree
+otherwise. All parties agree to exercise their best effort in good
+faith to resolve all disputes in mediation. If not, disputes shall be
+brought before the competent courts of France.
+
+8. Third party libraries
+
+The Software makes use of third-party libraries which had not been
+modified. These third-party components are made available under a
+number of different standard free software/open source licenses, and
+are mentioned below :
+* Coq standard library, LGPL-2.1, https://github.com/coq/coq
+* MathComp, CECILL-B, https://github.com/math-comp/math-comp
+* MathComp Analysis, CECILL-C, https://github.com/math-comp/analysis
+* MathComp Dioid, CECILL-C, https://github.com/math-comp/dioid
+* CoqEAL, MIT, https://github.com/CoqEAL/CoqEAL