DiscreteMath | Discrete Math Lessons |

IteratedBinops | Iterated Binary Operations |

SimpleMulFacts | Some handy lemmas about integer multiplication. |

num thy 1 | Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven. |

union | Non canonical functions (isl, outl, outr) for union type. |

int 2 | |

LogicSupplement | Some handy basic lemmas about propositions and about types. |

quot 1 | Support lemmas for quotient type. |

rel 1 | Common properties of binary relations. |

bool 1 | |

int 1 | |

well fnd | |

core | Some basic concepts defined type-theoretically. |