To play this document inside your browser use ALT-N and ALT-P.
If you get stack overflow
errors, try to use
Google Chrome
or Chromium
with the command line option --js-flags="--harmony-tailcalls".
You can
inside your browser and (edits are also saved when you close the window). Finally you can the file for offline editing.
Proof by case
Proof by induction
Eqtype
Addition
Subtraction
Order
One overloaded definition
Reflexivity
Antisymmetric
Transitivity
Scaling down
Addition
Multiplication
Conditional comparison
Division
odd
gcd & lcm
Coprime
Primality