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 save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Lesson 4 Arithmetics

• Order
• Division
• Primality

Reminder

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