<!doctype html>

<html>

<head>

<meta charset="utf-8">

<meta http-equiv="X-UA-Compatible" content="chrome=1">

<title>A Formal Proof of The Odd Order Theorem</title>

<link rel="stylesheet" href="stylesheets/styles.css">

<link rel="stylesheet" href="stylesheets/github-light.css">

<meta name="viewport" content="width=device-width">

<!--[if lt IE 9]>

<script src="//html5shiv.googlecode.com/svn/trunk/html5.js"></script>

<![endif]-->

</head>

<body>

<div class="wrapper">

<header>

<h1>A Formal Proof of The Odd Order Theorem</h1>

<p> A formalized and machine-checked proof,

using the Coq proof assistant</p>

<p class="view"><a href="https://github.com/math-comp/math-comp">View the Sources on GitHub <small>math-comp/math-comp</small></a></p>

</header>

<section>

<h3>

<a id="about" class="anchor" href="#about" aria-hidden="true"><span class="octicon octicon-link"></span></a>About</h3>

<p> Blah blah...

</p>

<p> TODO : a Q&A page

</p>

<h3>

<a id="borwsing" class="anchor" href="#releases"

aria-hidden="true"><span class="octicon

octicon-link"></span></a>Browsing

the files</h3>

<p> TODO

</p>

<h3>

<a id="releases" class="anchor" href="#releases"

aria-hidden="true"><span class="octicon

octicon-link"></span></a>Getting

the libraries</h3>

<p>

TODO

</p>

<h3>

<a id="contact" class="anchor" href="#contact" aria-hidden="true"><span class="octicon octicon-link"></span></a>Contact</h3>

<p>

Any question?

<a href="mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect">Subscribe to the ssreflect mailing list</a>

and let us know what you are using our libraries for, ask questions, etc.

You can also browse the <a href="https://sympa.inria.fr/sympa/arc/ssreflect">archives of the list</a> or consult the

<a href="https://sympa.inria.fr/sympa/info/ssreflect">general information page</a>.

</p>

<h3>

<a id="authors-and-contributors" class="anchor" href="#authors-and-contributors" aria-hidden="true"><span class="octicon octicon-link"></span></a>Authors and Contributors</h3>

<p> The Odd Order library, the Mathematical Components library and the

Ssreflect proof language are developed by the

<a href="http://www.msr-inria.fr/projects/mathematical-components-2/">Mathematical Components team</a>, at the

<a href="http://www.msr-inria.fr/">Inria -- Microsoft Research Joint Centre</a>.

</p>

<p style="text-align:center;">

<a href="http://www.msr-inria.fr/"><img src="./logo-MS-Research-Inria-Joint-Centre.png" alt="Microsoft Research - Inria Joint Centre" style="width:50%;margin-left:auto;margin-right:auto;"/></a>

</p>

</section>

<footer>

<p><small>Theme by <a href="https://github.com/orderedlist">orderedlist</a></small></p>

</footer>

</div>

<script src="javascripts/scale.fix.js"></script>

</body>

</html>