Require Import ssreflect ssrfun ssrnat seq ssrbool eqtype fintype choice finset.

Set Implicit Arguments.
Import Prenex Implicits.

Lemma all1s {T : eqType} {a : T} {s} {P : T -> Prop} :
  (forall b, b \in a :: s -> P b) -> P a /\ (forall b, b \in s -> P b).

Lemma leq_eq n m: n <= m -> m <= n -> n = m.

Lemma card_leq_inj (T T' : finType) (f : T -> T') : injective f -> #|T| <= #|T'|.

Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT.

Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|.

Lemma set1mem (T : finType) (A : {set T}) x : x \in A -> A = x |: A.

Lemma set_pick_size {F : finType} (X : {set F}) z : [pick z in X] = Some z -> #|X :\ z| < #|X|.

Definition surjective {X : eqType} {Y} (f : Y -> X) := forall x, exists w, f w == x.

Lemma surjectiveE (rT aT : finType) (f : aT -> rT) : surjective f -> #|codom f| = #|rT|.

Lemma surj_card_bij (T T' : finType) (f : T -> T') :
  surjective f -> #|T| = #|T'| -> bijective f.

Lemma size_induction {X : Type} (f : X -> nat) (p : X ->Prop) :
  ( forall x, ( forall y, f y < f x -> p y) -> p x) -> forall x, p x.

Lemma ptrans {T} (p1 p2 p3 : pred T) : p1 =i p2 -> p2 =i p3 -> p1 =i p3.

Lemma psym {T} (p1 p2 : pred T) : p1 =i p2 -> p2 =i p1.

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) := forall 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| F set0.

  Lemma lfp_ind (P : {set T} -> Type) : P set0 -> (forall 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.

Definition cr {X : choiceType} {Y : eqType} {f : X -> Y} (Sf : surjective f) y : X :=
  xchoose (Sf y).

Lemma crK {X : choiceType} {Y : eqType} {f : X->Y} {Sf : surjective f} x: f (cr Sf x) = x.

Section Quot.
  Variables (T : choiceType) (e : rel T).
  Hypothesis (e_refl: reflexive e) (e_sym : symmetric e) (e_trans : transitive e).

  Definition repr x := choose (e x) x.

  Lemma repr_rel x : e x (repr x).

  Lemma repr_idem x : repr x == repr (repr x).

  Definition quot := { x : T | x == repr x }.

  Definition Repr (x : T) : quot := Sub (repr x) (repr_idem x).

  Lemma Repr_id x y : reflect (Repr x = Repr y) (e x y).
End Quot.