ksk

Require Import List PeanoNat Arith Morphisms Setoid Recdef Lia.
Import ListNotations.

Set Implicit Arguments.

Ltac optimize db :=
  eexists; intros;
  match goal with
    |- ?X = ?Y =>
    let P := fresh in

ksk

(* Proof of Euclid' theorem *)
(* Constructive proof by Euclid himself *)

From mathcomp Require Import all_ssreflect.

Fixpoint primorial n :=
  if n is S m then (if prime n then n else 1) * primorial m else 1.

Notation "n `#" := (primorial n) (at level 2).

ksk

(* Zagier's one-sentence proof for the two-square theorem in Coq (SSReflect) *)
(* - D. Zagier, "A One-Sentence Proof That Every Prime p \equiv 1 (\mod 4) Is a Sum of Two Squares", 
     The American Mathematical Monthly, Vol. 97, No. 2 (Feb., 1990), p. 144 *)

Set Implicit Arguments. Unset Strict Implicit.
From mathcomp Require Import all_ssreflect.

Lemma odd_fixedpoints {X:eqType} (f:X->X) (D:seq X):
  uniq D -> (forall x, x \in D -> (f x \in D) && (f (f x) == x)) ->
  odd (size D) <-> odd (count [pred x | f x == x] D).