(* Author: Christian Doczkal *)
Require Import Relations.
Require Import tactics.

Set Implicit Arguments.
Import Prenex Implicits.

Lemma iter_fix T (F : T → T) x k n :
  iter k F x = iter k.+1 F x → k ≤ n → iter n F x = iter n.+1 F x.

Section FixPoint.
  Variable T :finType.
  Definition set_op := {set T} → {set T}.
  Definition mono (F : set_op) := ∀ p q : {set T} , p \subset q → F p \subset F q.

  Variable F : {set T} → {set T}.
  Hypothesis monoF : mono F.

  Definition lfp := iter #|T|.+1 F set0.

  Lemma lfp_ind (P : {set T} → Type) : P set0 → (∀ s , P s → P (F s)) → P lfp.

  Lemma iterFsub n : iter n F set0 \subset iter n.+1 F set0.

  Lemma iterFsubn m n : m ≤ n → iter m F set0 \subset iter n F set0.

  Lemma lfpE : lfp = F lfp.
End FixPoint.