Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset7.


Import Correspondence.
Import Bfunction.
Import Border.
Import Worder.
Import Cardinal.

Module FiniteSets.

Lemma cardinal_succ_pr3: forall x,
   succ (cardinal x) = x +c 1c.
Proof.
move=> x.
rewrite /card_one; apply card_plus_pr1; fprops.
apply (disjoint_with_singleton).
apply cardinal_irreflexive; apply cardinal_cardinal.
Qed.

Lemma cardinal_succ_pr4: forall x, is_cardinal x ->
   succ x = x +c 1c.
Proof.
move=> x cx; rewrite -{1}(cardinal_of_cardinal cx); apply cardinal_succ_pr3.
Qed.

Lemma finite_c_pr: forall x, finite_c x = (is_cardinal x & x <> succ x).
Proof.
move=> x; apply iff_eq => [ fx | [cx xsx]].
  have cx: is_cardinal x by fprops.
  split => //.
  move: fx => [p1 p2]; dneg h; red; rewrite -cardinal_equipotent -/(succ x).
  rewrite -h cardinal_of_cardinal//.
split; first by apply cardinal_ordinal.
dneg infx; red in infx; rewrite /succ -{1} (cardinal_of_cardinal cx); aw.
Qed.

Lemma infinite_c_pr: forall x, infinite_c x = (is_cardinal x & x = succ x).
Proof.
move=> x; rewrite /infinite_c /succ/infinite_o.
apply iff_eq; move=> [cx].
  rewrite -{4} (cardinal_of_cardinal cx); aw; move=> aux; ee.
rewrite -{1} (cardinal_of_cardinal cx); aw; move=> aux; ee.
Qed.

Lemma infinite_set_rw: forall x, infinite_set x = infinite_c (cardinal x).
Proof.
move => x; rewrite /infinite_c /infinite_set.
move: (cardinal_cardinal x) => h.
apply iff_eq; intuition.
Qed.

Lemma finite_dichot:forall x, is_cardinal x ->
  finite_c x \/ infinite_c x.
Proof.
move=> x cx; rewrite finite_c_pr infinite_c_pr.
case (equal_or_not x (succ x)); intuition.
Qed.

Lemma finite_dichot1: forall x,
  finite_set x \/ infinite_set x.
Proof.
move=> y; rewrite /finite_set infinite_set_rw; apply finite_dichot; fprops.
Qed.

Lemma succ_is_cardinal: forall a, is_cardinal (succ a).
Proof. move=> a; rewrite /succ; fprops. Qed.

Lemma cardinal_succ: forall a, cardinal (succ a) = succ a.
Proof. move=>a; apply (cardinal_of_cardinal (succ_is_cardinal a)). Qed.

Lemma succ_of_finite: forall x, finite_c x ->
  succ x = succ_o x.
Proof.
move=> x cx; rewrite /succ.
by rewrite (cardinal_of_cardinal (finite_cardinal_pr cx)).
Qed.

Theorem is_finite_succ: forall x, is_cardinal x ->
  (finite_c x) = (finite_c (succ x)).
Proof.
move=> x cx.
case (finite_dichot cx); last by rewrite infinite_c_pr; move => [_] <-.
move=> h; rewrite (succ_of_finite h); apply finite_o_pr.
Qed.

Lemma finite_le_infinite: forall a b,
  finite_c a -> infinite_c b -> a <=c b.
Proof.
move=> a b fa [cb ifb].
have ca: (is_cardinal a) by fprops.
move: (cardinal_ordinal cb) => ob.
red; ee.
move: fa; rewrite /finite_c -omega0_pr2 => ao.
rewrite omega0_pr1 // in ifb.
apply (ordinal_transitive ob (ifb _ ao)).
Qed.

Lemma finite_lt_infinite: forall a b,
  finite_c a -> infinite_c b -> a <c b.
Proof.
move=> a b fa ib; split; first by apply finite_le_infinite.
move=> ab; move: fa ib ; rewrite ab; move => [_ h1][_ h2]; contradiction.
Qed.

Theorem le_int_is_int: forall a b, finite_c b ->
  a <=c b -> finite_c a.
Proof.
move=> a b fb ab.
have ca: (is_cardinal a) by move: ab => [ca _].
case (finite_dichot ca) => // ia.
move: (finite_lt_infinite fb ia) => ba; co_tac.
Qed.

Definition Bnat := omega0.

Lemma inc_Bnat: forall a, inc a Bnat = finite_c a.
Proof. by move=> a; rewrite /Bnat omega0_pr2. Qed.

Hint Rewrite inc_Bnat : bw.

Lemma Bnat_is_cardinal: forall x, inc x Bnat -> is_cardinal x.
Proof. move =>x; bw; fprops. Qed.

Lemma Bnat_cardinal: forall x, inc x Bnat -> cardinal x = x.
Proof. by move => x xB; apply cardinal_of_cardinal; apply Bnat_is_cardinal. Qed.

Hint Resolve Bnat_is_cardinal : fprops.

Lemma Bsucc_rw: forall x, inc x Bnat ->
   succ x = x +c 1c.
Proof.
by move=> x fx; apply cardinal_succ_pr4; fprops.
Qed.

Lemma BS_succ: forall x, inc x Bnat -> inc (succ x) Bnat.
Proof. move=> x; bw => aux; rewrite - is_finite_succ ; fprops. Qed.

Ltac hprops := auto with hprops.
Hint Resolve BS_succ: hprops.

Lemma Bnat0_unit_sumr: forall x, inc x Bnat -> x +c 0c = x.
Proof. by move=> x xB; apply zero_unit_sumr; fprops. Qed.
Lemma Bnat0_unit_suml: forall x, inc x Bnat -> 0c +c x = x.
Proof. by move=> x xB; apply zero_unit_suml; fprops. Qed.

Lemma le_int_in_Bnat: forall a b, a <=c b -> inc b Bnat -> inc a Bnat.
Proof. move=>a b ab; bw=> bi; apply (le_int_is_int bi ab). Qed.

Ltac Bnat_tac :=
  match goal with
    | H1: finite_c ?b, H2: cardinal_le ?a ?b |- finite_c ?a
      => apply (le_int_is_int H1 H2)
    | H1: cardinal_le ?a ?b, H2:inc ?b Bnat |- inc ?a Bnat
      => apply (le_int_in_Bnat H1 H2)
    | H1: cardinal_lt ?a ?b, H2:inc ?b Bnat |- inc ?a Bnat
      => move: H1 => [H1 _ ]; apply (le_int_in_Bnat H1 H2)
end.

Definition card_three := succ card_two.
Definition card_four := succ card_three.
Notation "3 'c'" := card_three.
Notation "4 'c'" := card_four.

Lemma succ_zero: succ 0c = 1c.
Proof. rewrite /succ succ_o_zero; apply cardinal_of_cardinal; apply cardinal1.
Qed.

Lemma succ_one: succ 1c = 2c.
Proof. rewrite /succ succ_o_one; apply cardinal_of_cardinal; apply cardinal2.
Qed.

Lemma inc0_Bnat: inc 0c Bnat.
Proof. rewrite inc_Bnat; apply finite_zero. Qed.

Lemma inc1_Bnat: inc 1c Bnat.
Proof. move: inc0_Bnat; rewrite -succ_zero; hprops. Qed.

Lemma inc2_Bnat: inc 2c Bnat.
Proof. move: inc1_Bnat; rewrite -succ_one; hprops. Qed.

Lemma inc3_Bnat: inc 3c Bnat.
Proof. move: inc2_Bnat; rewrite /card_three; hprops. Qed.

Lemma inc4_Bnat: inc 4c Bnat.
Proof. move: inc3_Bnat; rewrite /card_four; hprops. Qed.

Hint Resolve inc0_Bnat inc1_Bnat inc2_Bnat: fprops.

Lemma two_plus_two: 2c +c 2c = 4c.
Proof.
rewrite /card_four (Bsucc_rw inc3_Bnat).
rewrite /card_three (Bsucc_rw inc2_Bnat).
rewrite -card_plusA -card_two_pr //.
Qed.

Lemma two_times_n: forall n, 2c *c n = n +c n.
Proof.
move=> n; set (m:= cardinal n).
have cm: is_cardinal m by rewrite /m;fprops.
have nn: card_plus n n= card_plus m m
   by rewrite /m; apply cardinal_sum_pr2; fprops.
have n2:card_mult card_two n= card_mult card_two m.
   by rewrite ? card_mult_pr1 /m; aw; apply equipotent_product; fprops.
rewrite nn n2 -card_two_pr cardinal_distrib_prod_sum2; aw.
Qed.

Lemma two_times_two: 2c *c 2c = 4c.
Proof. rewrite - two_plus_two; apply two_times_n. Qed.

Lemma power_2_4: 2c ^c 4c = 4c ^c 2c.
Proof.
by rewrite -{2} two_times_two power_of_prod2 -two_plus_two power_of_sum2.
Qed.

Lemma is_le_succ0: forall a, is_cardinal a ->
  a <=c (succ a).
Proof.
move=> a ca; rewrite cardinal_succ_pr4 // cardinal_le_when_complement //.
  exists card_one; split=>//; apply cardinal1.
fprops.
Qed.

Lemma is_finite_in_sum: forall a b, is_cardinal b ->
  finite_c (a +c b) -> finite_c b.
Proof.
move=> a b cb; rewrite ! finite_c_pr; move=> [cp fcp]; split=>//.
rewrite (cardinal_succ_pr4 cb).
by dneg bs; rewrite (cardinal_succ_pr4 cp) -card_plusA -bs.
Qed.

Lemma is_finite_in_sum2: forall a b, is_cardinal a ->
  finite_c (a +c b) -> finite_c a.
Proof.
move=> a b ca; rewrite card_plusC.
move=> fp;apply (is_finite_in_sum ca fp).
Qed.

Lemma Bnat_in_sum: forall a b, is_cardinal b ->
  inc (a +c b) Bnat ->inc b Bnat.
Proof. move=> a b cb; bw; move=> h; apply (is_finite_in_sum cb h). Qed.

Lemma Bnat_in_sum2: forall a b, is_cardinal a ->
  inc (a +c b) Bnat ->inc a Bnat.
Proof. move=> a b ca; bw; move=> h; apply (is_finite_in_sum2 ca h). Qed.

Lemma cardinal_complement2: forall a b, inc a Bnat ->
  b <=c a -> inc (cardinal (complement a b)) Bnat.
Proof.
move=> a b aB leab; move: (cardinal_complement1 leab) => aux.
have cc: is_cardinal ((cardinal (complement a b))) by fprops.
rewrite -aux card_plusC in aB.
exact (Bnat_in_sum2 cc aB).
Qed.

Lemma Bnat_in_product: forall a b, is_cardinal a ->
  b <> 0c -> inc (a *c b) Bnat -> inc a Bnat.
Proof.
move=> a b ca nzb.
have on: (1c <=c (cardinal b)).
  apply one_small_cardinal; first by fprops.
  by move=> cz; move: (cardinal_nonemptyset cz); apply nzb .
have ->: a *c b = a *c (cardinal b).
  by apply card_mult_pr2; fprops;rewrite double_cardinal.
rewrite -(cardinal_complement1 on).
rewrite /succ cardinal_distrib_prod_sum3 one_unit_prodr //.
apply (Bnat_in_sum2 ca).
Qed.

Lemma BS_nsucc: forall x, is_cardinal x -> inc (succ x) Bnat -> inc x Bnat.
Proof.
move=> x xs sB.
case (finite_dichot xs); first by rewrite inc_Bnat.
by rewrite infinite_c_pr; move=> [_] ->.
Qed.

Definition predc := union.

Lemma predc_pr: forall n, inc n Bnat -> n <> 0c ->
  (inc (predc n) Bnat & n = succ (predc n)).
Proof.
move=> n; rewrite inc_Bnat /finite_c /card_zero finite_succ => p1 p2.
case p1; first by move=> aux;elim p2 =>//.
move=> [y [fy ns]].
have oy: (is_ordinal y) by move: fy => [ok _].
move: (ordinal_predecessor oy).
rewrite /predc; rewrite -ns; move => <-.
rewrite (succ_of_finite fy) inc_Bnat; ee.
Qed.

Lemma is_le_succ: forall a, inc a Bnat -> a <=c (succ a).
Proof. move=> a aB; apply is_le_succ0; fprops. Qed.

Lemma is_lt_succ: forall a, inc a Bnat -> a <c (succ a).
Proof.
 move=> a aB; split; first by apply is_le_succ.
by move: aB; bw; rewrite finite_c_pr; move=> [h].
Qed.

Lemma cardinal_complement3: forall a b, inc a Bnat -> b <c a ->
  (cardinal (complement a b)) <> 0c.
Proof.
move => a b aB [leba neba].
move: (cardinal_complement2 aB leba) (cardinal_complement1 leba).
set c := (cardinal _) => cB pac.
dneg cs; move: pac; rewrite cs zero_unit_sumr//; co_tac.
Qed.

Theorem lt_is_le_succ: forall a n, inc n Bnat ->
  a <c (succ n) = a <=c n.
Proof.
move=> a n fn; apply iff_eq; last by move: (is_lt_succ fn)=> p1 p2; co_tac.
move: (BS_succ fn) => sn ltas; move: (ltas) => [leas nas].
move: (cardinal_complement2 sn leas) (cardinal_complement1 leas)
(cardinal_complement3 sn ltas).
set c := (cardinal (complement (succ n) a)) => cB pac nzc.
move: (predc_pr cB nzc)=> [cp pv].
move: pac; rewrite pv (Bsucc_rw cp) card_plusA (Bsucc_rw fn) => h.
have <-: (card_plus a (predc c) = n) by apply succ_injective; fprops.
apply sum_increasing3; [ co_tac | fprops].
Qed.

Hint Rewrite lt_is_le_succ : sw.

Lemma lt_is_le_succ1: forall a b, inc b Bnat ->
  a <=c (succ b) -> a <> (succ b) -> a <=c b.
Proof. move=> a b fb leas asb; rewrite -lt_is_le_succ//. Qed.

Lemma lt_n_succ_le1: forall a b, is_cardinal a -> inc b Bnat ->
  (a <=c b) = (succ a <=c succ b).
Proof.
move=> a b ca fb; apply iff_eq => h.
  have cb: is_cardinal b by fprops.
  rewrite ! cardinal_succ_pr4 //.
  apply (sum_increasing2 h (cardinal_le_reflexive cardinal1)).
rewrite - lt_is_le_succ //.
move: (is_le_succ0 ca) => le1.
split; first by apply (cardinal_le_transitive le1 h).
move=> aux; rewrite -aux in h.
move: (BS_succ fb).
by rewrite -aux inc_Bnat finite_c_pr (cardinal_antisymmetry1 h le1); intuition.
Qed.

Lemma succ_nonzero:forall n, succ n <> 0c.
Proof.
move=> n;rewrite /succ/succ_o /card_zero.
apply cardinal_nonemptyset1; exists n; fprops.
Qed.

Lemma predc_pr1: forall n, is_cardinal n -> predc (succ n) = n.
Proof.
move=> n cn.
case (finite_dichot cn).
  move: cn => [cn _ aux];
  by rewrite succ_of_finite //; symmetry;apply ordinal_predecessor.
move => ifn; move: (ifn).
rewrite infinite_c_pr; move=> [_ h]; rewrite -h.
apply (infinite_card_limit1 ifn).
Qed.

Lemma predc_pr2: forall n, inc n Bnat -> predc (succ n) = n.
Proof.
move=> n nb; apply predc_pr1; fprops.
Qed.

Lemma predc_pr3: forall n, inc n Bnat ->
  n = card_zero \/ exists m, inc m Bnat & n = succ m.
Proof.
move=> n nB; case: (equal_or_not n card_zero); first by intuition.
move=> ne; right; exists (predc n); move: (predc_pr nB ne); bw.
Qed.

Lemma succ_positive: forall a, 0c <c (succ a).
Proof.
move=> a; split; first by apply zero_smallest; apply succ_is_cardinal.
move: (@succ_nonzero a); intuition.
Qed.

Lemma zero_lt_one: 0c <c 1c.
Proof. rewrite - succ_zero; apply succ_positive. Qed.

Lemma zero_le_one: 0c <=c 1c.
Proof. by move: zero_lt_one => [res _]. Qed.

Lemma cardinal_lt20: 0c <c 2c.
Proof. rewrite -succ_one lt_is_le_succ; fprops; apply zero_le_one. Qed.

Lemma one_small_cardinal2: forall a, is_cardinal a ->
  1c <=c a = (a <> 0c).
Proof.
move=> a ca; apply iff_eq.
  move=> lea az; rewrite az in lea.
  move: (cardinal_antisymmetry1 lea zero_le_one); apply card_one_not_zero.
by move=> h; apply one_small_cardinal.
Qed.

Lemma lt_n_succ_le0: forall a b, is_cardinal a -> inc b Bnat ->
  (succ a <=c b) = a <c b.
Proof.
move=> a b ca fb; symmetry.
case (equal_or_not b card_zero).
  move=> ->; apply iff_eq => h.
    elim (zero_smallest1 h).
  have lts:(cardinal_lt (succ a) card_zero).
    split=>//; apply (succ_nonzero (n:=a)).
  elim (zero_smallest1 lts).
move=> nzb; move: (predc_pr fb nzb)=> [pb pv].
rewrite pv -lt_n_succ_le1 //; srw.
Qed.

Hint Rewrite lt_n_succ_le0 : sw.

Lemma lt_n_succ_le: forall a b, inc a Bnat -> inc b Bnat ->
  (succ a <=c b) = a <c b.
Proof. move=> a b aB bB; srw; fprops. Qed.

Lemma sub_finite_set: forall x y, sub x y -> finite_set y ->
  finite_set x.
Proof.
rewrite/finite_set=> x y xy fy; apply (le_int_is_int fy (sub_smaller xy)).
Qed.

Lemma strict_sub_smaller: forall x y, sub x y -> finite_set y ->
  x<> y -> (cardinal x) <c (cardinal y).
Proof.
move=> x y sxy fsy nxy.
have ssxy:(strict_sub x y) by split.
move: (strict_sub_nonempty_complement ssxy) =>[u uc].
set (z:= complement y (singleton u)).
have szy: sub z y by rewrite /z; apply sub_complement.
have sxz: sub x z.
   move=> t tx; rewrite /z; srw; split; first by apply sxy.
   aw; dneg tu; move: uc; rewrite -tu; srw. move=>[_ ntx]; contradiction.
move ss:(sub_smaller sxz)=> lexz.
have ->: (cardinal y = succ (cardinal z)).
  rewrite /z -cardinal_succ_pr1 - tack_on_complement //.
  move: uc; srw; intuition.
srw; bw; apply (sub_finite_set szy fsy).
Qed.

Lemma emptyset_finite: finite_set emptyset.
Proof. red;rewrite cardinal_emptyset; rewrite -inc_Bnat ; apply inc0_Bnat.
Qed.

Lemma strict_sub_smaller1: forall y,
  (forall x, sub x y -> x<> y -> (cardinal x) <c (cardinal y)) ->
  finite_set y.
Proof.
move=> y h.
case (emptyset_dichot y).
  move => ->; apply emptyset_finite.
move=> [u uy].
set (z:=complement y (singleton u)).
have zy: sub z y by rewrite /z; apply sub_complement.
have yt: y = tack_on z u by rewrite /z; apply tack_on_complement.
move: (cardinal_succ_pr1 y u); rewrite -/z -yt => cy.
have cc: is_cardinal (cardinal z) by fprops.
red; rewrite cy -is_finite_succ // finite_c_pr; split => //.
have nzy:z <> y.
  move=> ezy; move: uy; rewrite -ezy /z; srw; aw.
  by move => [_ neq]; apply neq.
move: (h _ zy nzy); rewrite cy.
rewrite /cardinal_lt ; intuition.
Qed.

Lemma finite_image: forall f, is_function f -> finite_set (source f) ->
  finite_set (image_of_fun f).
Proof.
move=> f ff fs; move: (image_smaller_cardinal ff)=> cle.
apply (le_int_is_int fs cle).
Qed.

Lemma finite_image_by: forall f A, is_function f -> sub A (source f) ->
  finite_set A -> finite_set (image_by_fun f A).
Proof.
move=> f A ff sAsf fsA.
set (g:= restriction1 f A).
have [fg sg]: (surjection g) by rewrite /g; apply restriction1_surjective.
have <-:(image_of_fun g = image_by_fun f A).
  rewrite sg /g /restriction1; aw.
apply finite_image=>//.
rewrite /g/restriction1; aw.
Qed.

Lemma finite_fun_image: forall a f, finite_set a ->
  finite_set (fun_image a f).
Proof.
move=> a f fsa;
have [fb sj]: (surjection (BL f a (fun_image a f))).
  apply bl_surjective.
    by move=> t ta; aw; exists t.
  move=> y; aw.
awi sj; rewrite -sj;apply finite_image=>//; aw.
Qed.

Lemma finite_range: forall f, fgraph f -> finite_set(domain f) ->
  finite_set(range f).
Proof.
move=> f fgf fsd.
have ff: (is_function (corresp (domain f) (range f) f)).
  by apply is_function_pr; fprops.
have ->: (range f = image_of_fun (corresp (domain f)(range f) f)).
  by rewrite (image_of_fun_range ff); aw.
apply finite_image=>//; aw.
Qed.

Lemma finite_graph_domain: forall f, fgraph f ->
  finite_set f -> finite_set (domain f).
Proof. move=> f fgf; rewrite /domain; apply finite_fun_image.
Qed.

Lemma finite_graph_range: forall f, fgraph f ->
  finite_set f -> finite_set (range f).
Proof. by move=> f fgf fsf;rewrite/range; apply finite_fun_image.
Qed.

Lemma finite_domain_graph: forall f, fgraph f ->
  finite_set (domain f) -> finite_set f.
Proof.
by move=> f fgf fsd;rewrite -(L_recovers fgf) /L; apply finite_fun_image.
Qed.

Lemma bijective_if_same_finite_c_inj: forall f,
  cardinal (source f) = cardinal (target f) -> finite_set (source f) ->
  injection f -> bijection f.
Proof.
move=> f csftf fs injf; split=>//; split; first by fct_tac.
have fst: (finite_set (target f)) by red; ue.
have sit: (sub (image_of_fun f) (target f)).
  apply sub_image_target; fct_tac.
ex_middle it.
move:(strict_sub_smaller sit fst it) => [cle ne].
elim ne; transitivity (cardinal (source f))=>//.
symmetry; aw.
exists (restriction_to_image f).
split; first by apply (restriction_to_image_bijective injf).
by rewrite /restriction_to_image /restriction2; aw.
Qed.

Lemma sub_image_of_fun: forall f x, is_function f -> sub x (source f) ->
  sub (image_by_fun f x) (image_of_fun f).
Proof.
move=> f x ff sxf; rewrite /image_by_fun/image_of_fun.
by apply image_by_increasing.
Qed.

Lemma bijective_if_same_finite_c_surj: forall f,
  cardinal (source f) = cardinal (target f) -> finite_set (source f) ->
  surjection f -> bijection f.
Proof.
move=> f cstf fsf sf.
move: (exists_right_inv_from_surj sf)=> [g rig].
move: (source_right_inverse rig) =>sg.
move: (right_inverse_injective rig)=> ig.
move: rig =>[co c]; move: (co) => [_ [s t]].
have csftf: (cardinal (source g) = cardinal (target g)).
   by rewrite sg -t.
have fss: finite_set (source g).
  by red; rewrite sg -cstf.
move: (bijective_if_same_finite_c_inj csftf fss ig)=> bg.
have bc: (bijection (compose f g)) by rewrite c; apply identity_bijective.
apply (bij_left_compose co bc bg).
Qed.

Definition Bnat_order := graph_on cardinal_le Bnat.
Definition Bnat_le x y := inc x Bnat & inc y Bnat & x <=c y.
Definition Bnat_lt x y := Bnat_le x y & x<>y.

Notation "x <=N y" := (Bnat_le x y) (at level 50).
Notation "x <N y" := (Bnat_lt x y) (at level 50).

Lemma Bnat_order_substrate: substrate Bnat_order = Bnat.
Proof.
have alc: (forall x, inc x Bnat -> is_cardinal x) by move=> x xn; fprops.
by move: (wordering_cardinal_le_pr alc)=> [].
Qed.

Lemma Bnat_order_worder: worder Bnat_order.
Proof.
have alc: (forall x, inc x Bnat -> is_cardinal x) by move=> x xn; fprops.
by move: (wordering_cardinal_le_pr alc)=> [].
Qed.

Lemma Bnat_order_le: forall x y,
  gle Bnat_order x y = x <=N y.
Proof. by move=> x y; rewrite / Bnat_order; aw; rewrite /gle graph_on_rw1.
Qed.

Lemma Bnat_wordered : forall X, sub X Bnat -> nonempty X ->
  inc 0c X \/
  (exists a, inc a Bnat & inc (succ a) X & ~ (inc a X)).
Proof.
move=> X Xb neX.
move: Bnat_order_worder=> [or wor].
rewrite Bnat_order_substrate in wor.
have aux: sub X (substrate Bnat_order) by rewrite Bnat_order_substrate.
move: (wor _ Xb neX) => [x []]; aw; move=> xX xle.
case (predc_pr3 (Xb _ xX)) => h.
  by left; rewrite -h.
move: h => [c [cn xs]]; right; exists c; split=>//.
split; first by ue.
move=> xC; move: (xle _ xC); aw.
rewrite Bnat_order_le/ Bnat_le; move=> [xB [cB lexc]].
move: (is_lt_succ cB); rewrite -xs=> lecx; co_tac.
Qed.

Lemma Bnat_interval_cc_pr: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_cc Bnat_order a b) = (a <=N x & x <=N b).
Proof.
move=> a b x aB bB.
rewrite /interval_cc Bnat_order_substrate Z_rw ! Bnat_order_le.
rewrite /Bnat_le; apply iff_eq; intuition.
Qed.

Lemma Bnat_interval_co_pr: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_co Bnat_order a b) = (a <=N x & x <N b).
Proof.
move=> a b c aB bB.
rewrite/ Bnat_lt/interval_co Bnat_order_substrate.
rewrite Z_rw /glt ! Bnat_order_le /Bnat_le; apply iff_eq; intuition.
Qed.

Lemma Bnat_interval_cc_pr1: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_cc Bnat_order a b) = (a <=c x & x <=c b).
Proof.
move=> a b x aB bB; rewrite Bnat_interval_cc_pr // /Bnat_le.
apply iff_eq; first by intuition.
move=> [ax bx].
have xB: inc x Bnat by Bnat_tac.
ee.
Qed.

Lemma Bnat_interval_co_pr1: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_co Bnat_order a b) = (a <=c x & x <c b).
Proof.
move=> a b x aB bB.
rewrite Bnat_interval_co_pr // /Bnat_lt /Bnat_le /cardinal_lt.
apply iff_eq; first by intuition.
move=> [ax [bx xb]];move:(le_int_in_Bnat bx bB)=> xB.
intuition.
Qed.

Lemma cardinal_c_induction: forall r:Set -> Prop,
  (r 0c) -> (forall n, inc n Bnat-> r n -> r (succ n))
  -> (forall n, inc n Bnat -> r n).
Proof.
move=> r r0 ri n nN; set (X:= Zo Bnat (fun z => ~ (r z))).
ex_middle nrn.
have sB: sub X Bnat by rewrite /X; apply Z_sub.
have ns:nonempty X by exists n; rewrite /X;apply Z_inc.
case: (Bnat_wordered sB ns).
  rewrite /W Z_rw; move => [_ nr0]; contradiction.
move=> [a [an []]]; rewrite /X 2! Z_rw; move=> [saB nrs] na.
by elim na; clear na;split=>//; dneg ra; apply ri.
Qed.

Lemma cardinal_c_induction1: forall r:Set -> Prop,
  let s:= fun n => forall p, inc n Bnat -> inc p Bnat ->
    p <c n -> r p in
  (forall n, inc n Bnat -> s n -> r n) ->
  (forall n, inc n Bnat -> r n).
Proof.
move=> r s si n fn; apply si=>//.
apply cardinal_c_induction=>//.
  rewrite /s=> p f0 fp np; elim (zero_smallest1 np).
move=> m fm sm p fsp fp lp.
case (equal_or_not p m); first by move=>->; apply si =>//.
move=> pm; apply sm=>//; split=>//; move: lp; srw.
Qed.

Lemma cardinal_c_induction2: forall (r:Set -> Prop) k,
  inc k Bnat -> r k ->
  (forall n, inc n Bnat -> k <=c n -> r n -> r (succ n))
  -> (forall n, inc n Bnat -> k <=c n -> r n).
Proof.
move=> r k fk rk ri n fn kn.
move: n fn kn; apply: cardinal_c_induction.
  by move=> h; rewrite - (zero_smallest2 h).
move=> m fm sm; case (equal_or_not k (succ m)).
  by move => <-.
move => ks ksm; move: (lt_is_le_succ1 fm ksm ks)=> lekm.
by apply ri=>//; apply sm.
Qed.

Lemma cardinal_c_induction3: forall (r:Set -> Prop) a b,
  inc a Bnat -> inc b Bnat -> r a ->
  (forall n, a <=c n -> n <c b -> r n -> r (succ n))
  -> (forall n, a <=c n -> n <=c b -> r n).
Proof.
move=> r a b fa fb ra ri n an nb.
have nB: inc n Bnat by Bnat_tac.
move: n nB an nb; apply: cardinal_c_induction.
   by move => az _; rewrite -(zero_smallest2 az).
move=> m fm sm am; srw; fprops => mb.
case (equal_or_not a (succ m)).
   by move => <-.
move=> asm; move: (lt_is_le_succ1 fm am asm)=> leam.
apply ri=>//.
apply sm=>//; by move: mb=> [mb _].
Qed.

Lemma cardinal_c_induction4: forall (r:Set -> Prop) a b,
  inc a Bnat -> inc b Bnat -> r b ->
  (forall n, a <=c n -> n <c b -> r (succ n) -> r n)
  -> (forall n, a <=c n -> n <=c b -> r n).
Proof.
move=> r a b fa fb rb ti n an nb.
set (q := fun n => ~ (r n)).
case (p_or_not_p (r n))=>// nrn.
have fc:inc n Bnat by Bnat_tac.
have qi: (forall m, cardinal_le n m -> cardinal_lt m b -> q m -> q (succ m)).
  rewrite /q;move=> m nm mb qm; dneg rs; apply ti=> //; co_tac.
move: (cardinal_c_induction3 fc fb nrn qi) => aux.
have: (q b) by apply aux=>//; fprops.
rewrite /q => nrb; contradiction.
Qed.

Lemma cardinal_c_induction3_v: forall (r:Set -> Prop) a b,
  inc a Bnat -> inc b Bnat -> r a ->
  (forall n, inc n (interval_co Bnat_order a b) -> r n -> r (succ n))
  -> (forall n, inc n (interval_cc Bnat_order a b) -> r n).
Proof.
move=>r a b aB bB ra ri m.
have ri': (forall n, a <=c n -> n <c b -> r n -> r (succ n)).
  by move=> n an nb;apply ri; rewrite Bnat_interval_co_pr1//.
rewrite Bnat_interval_cc_pr1 //; move=> [am mb].
apply (cardinal_c_induction3 aB bB)=>//.
Qed.

Lemma cardinal_c_induction4_v: forall (r:Set -> Prop) a b,
  inc a Bnat -> inc b Bnat -> r b ->
  (forall n, inc n (interval_co Bnat_order a b) -> r (succ n) -> r n)
  -> (forall n, inc n (interval_cc Bnat_order a b) -> r n).
Proof.
move=> r a b aB bB rb ri m.
have ri':(forall n, a <=c n -> n <c b -> r (succ n) -> r n).
  move=> n an bn; apply ri; rewrite Bnat_interval_co_pr1 //.
rewrite Bnat_interval_cc_pr1 //; move=> [am mb].
apply (cardinal_c_induction4 aB bB)=>//.
Qed.

Lemma tack_on_finite: forall X x,
  finite_set X -> finite_set (tack_on X x).
Proof.
move=>X x fX; case (inc_or_not x X) => h.
suff: (tack_on X x= X) by move=> ->.
  by apply tack_on_when_inc.
red; rewrite cardinal_succ_pr //.
rewrite - is_finite_succ //; fprops.
Qed.

Lemma singleton_finite: forall x, finite_set(singleton x).
Proof.
move=> x;red;rewrite cardinal_singleton; rewrite -inc_Bnat; apply inc1_Bnat.
Qed.

Lemma doubleton_finite: forall x y, finite_set(doubleton x y).
Proof.
move=> x y.
have ->: (doubleton x y = tack_on (singleton x) y).
  by set_extens z; aw; rewrite doubleton_rw.
apply tack_on_finite; apply singleton_finite.
Qed.

Lemma tack_if_succ_card: forall x n, is_cardinal n -> cardinal x = succ n ->
  exists u, exists v, x = tack_on u v & ~(inc v u) & cardinal u = n.
Proof.
move=> x n cn cx.
case (emptyset_dichot x) => h.
  move: cx;rewrite h cardinal_emptyset =>h'.
  symmetry in h'; elim (succ_nonzero h').
move: h=> [y yx].
have xt: (x = tack_on (complement x (singleton y)) y).
 by apply tack_on_complement.
exists (complement x (singleton y)); exists y;split =>//.
split; first by apply not_inc_complement_singleton.
move: (cardinal_succ_pr1 x y).
rewrite -xt; move=> h; rewrite h in cx.
apply succ_injective1; fprops.
Qed.

Lemma finite_set_induction0: forall s:Set -> Prop,
  s emptyset -> (forall a b, s (a) -> ~(inc b a) -> s (tack_on a b)) ->
  forall x, finite_set x -> s x.
Proof.
move=> s se si x fx.
set (r:= fun n => forall x, cardinal x = n-> s x).
have r0: (r card_zero) by rewrite /r => y h; rewrite (cardinal_nonemptyset h).
have ri: forall n, inc n Bnat -> r n -> r (succ n).
  move=> n fn rn.
  have cn: (is_cardinal n) by fprops.
  move=> y yp; move: (tack_if_succ_card cn yp) => [u [v [yt [nvu cu]]]].
   by rewrite yt; apply si=>//; apply rn.
move: (cardinal_c_induction r0 ri) => hr.
red in fx; rewrite - inc_Bnat in fx; by move: (hr _ fx); apply.
Qed.

Lemma finite_set_induction: forall s:Set -> Prop,
  s emptyset -> (forall a b, s (a) -> s (tack_on a b)) ->
  forall x, finite_set x -> s x.
Proof.
move =>s se si x fs; apply (finite_set_induction0 (s:=s))=>//.
by move=> a b sa _; apply si.
Qed.

Lemma finite_set_induction1: forall (A B:Set -> Prop) x,
  (A emptyset -> B emptyset)
  -> (forall a b, (A a -> B a) -> A(tack_on a b) -> B(tack_on a b))
  -> finite_set x -> A x -> B x.
Proof.
move=> A B x h1 h2 fs.
set (s:= fun x => A x -> B x); apply (finite_set_induction (s:=s)h1)=>//.
Qed.

Lemma finite_set_induction2: forall (A B:Set -> Prop) x,
  (forall a, A (singleton a) -> B (singleton a))
  -> (forall a b, (A a -> nonempty a -> B a) ->
    nonempty a -> A(tack_on a b) -> B(tack_on a b))
  -> finite_set x -> A x -> nonempty x -> B x.
Proof.
move=> A B x fA fr.
set (s:= fun x => A x -> nonempty x -> B x).
apply (finite_set_induction (s:=s)).
  rewrite /s; move=> _ [t te]; elim (emptyset_pr te).
move=> a b sa.
case (emptyset_dichot a) => pa.
  have ->: (tack_on a b = singleton b).
    rewrite pa;set_extens y; aw; auto; case=>//; case;case.
  by move => h _; apply fA.
move=> h h'; apply fr=>//.
Qed.

Lemma plus_via_succ: forall a b, inc b Bnat ->
  a +c (succ b) = succ (a +c b).
Proof.
move=> a b bB.
rewrite (Bsucc_rw bB) card_plusA.
rewrite cardinal_succ_pr4 //; fprops.
Qed.

Lemma plus_via_succ1: forall a b, inc a Bnat ->
   (succ a) +c b = succ (a +c b).
Proof. by move=> a b aB; rewrite card_plusC (plus_via_succ _ aB) card_plusC.
Qed.

Lemma mult_via_plus: forall a b, inc a Bnat -> inc b Bnat ->
  a *c (succ b) = (a *c b) +c a.
Proof.
 move=> a b aB bB; rewrite (Bsucc_rw bB) cardinal_distrib_prod_sum3.
rewrite (one_unit_prodr (Bnat_is_cardinal aB)) //.
Qed.

Lemma BS_plus: forall a b, inc a Bnat -> inc b Bnat ->
  inc (a +c b) Bnat.
Proof.
move=> a b; move=> aB bB.
move: b bB; apply cardinal_c_induction; first by aw;fprops.
move=> n fn fan.
rewrite (plus_via_succ a fn); hprops.
Qed.

Lemma BS_mult: forall a b, inc a Bnat -> inc b Bnat ->
  inc (a *c b) Bnat.
Proof.
move=> a b aB bB.
move: b bB; apply cardinal_c_induction.
  aw; rewrite zero_prod_absorbing; fprops.
by move=> n nB mB; rewrite mult_via_plus; fprops; apply BS_plus.
Qed.

Hint Resolve BS_plus BS_mult: hprops.
Hint Resolve inc0_Bnat inc1_Bnat inc2_Bnat: hprops.

Lemma pow_succ: forall a b, inc b Bnat ->
  a ^c (succ b) = (a ^c b) *c a.
Proof.
move=> a b bB; rewrite (Bsucc_rw bB) power_of_sum2;apply card_mult_pr2 =>//.
rewrite (power_x_1c a); apply double_cardinal.
Qed.

Lemma BS_pow: forall a b, inc a Bnat -> inc b Bnat ->
  inc (a ^c b) Bnat.
Proof.
move=> a b aB bB.
move: b bB; apply cardinal_c_induction.
  rewrite power_x_0; fprops.
move=> n nB mB; rewrite pow_succ; hprops.
Qed.

Hint Resolve BS_pow: hprops.

Lemma finite_set_induction3: forall (p: Set -> Set -> Prop) E X,
  (forall a b, inc a E -> inc b E -> exists y, p (doubleton a b) y) ->
  (forall a b x y, sub a E -> inc b E -> p a x -> p (doubleton x b) y->
    p (tack_on a b) y) ->
  (forall X x, sub X E -> nonempty X -> p X x -> inc x E) ->
  nonempty X -> finite_set X -> sub X E -> exists x, p X x.
Proof.
move=> p E X p1 p2 p3 neX fsX XE.
apply (@finite_set_induction2 (fun X=> sub X E)
  (fun X => exists x, p X x)) => //.
  move=> a aE.
  have aE': inc a E by apply aE; fprops.
  by rewrite -doubleton_singleton; apply p1.
move=> a b p4 nea st.
have saE: sub a E by apply sub_trans with (tack_on a b); fprops.
have bE: inc b E by apply st;fprops.
move: (p4 saE nea)=> [y py].
move: (p3 _ _ saE nea py) => yE.
move: (p1 _ _ yE bE)=> [z pz].
exists z; apply: (p2 _ _ _ _ saE bE py pz).
Qed.

Lemma finite_subset_directed_bounded: forall r X,
  right_directed r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> bounded_above r X.
Proof.
move=> r X [or rr] fsX sX neX.
move: neX fsX sX.
apply finite_set_induction3 => //.
  move=> a b x y asr bsr [xsr ubx] [yser upy].
  split =>//.
  move: (upy _ (doubleton_first x b)) => xy.
  move: (upy _ (doubleton_second x b)) => lby.
  move=> t; aw; case.
    move => ta; move: (ubx _ ta)=> aux; order_tac.
  by move=>->.
by move => Y x Ysr neY [sr uYx].
Qed.

Lemma finite_subset_lattice_inf: forall r X,
  lattice r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, greatest_lower_bound r X x.
Proof.
move=> r X [or lr] fsX Xsr neX.
move: neX fsX Xsr.
apply finite_set_induction3 => //.
    move=>a b asr bsr; by move: (lr _ _ asr bsr)=> [p1 p2].
  move=> a b x y asr bsr sax.
  have st: sub (tack_on a b) (substrate r) by apply tack_on_sub.
  awi sax =>//; move:sax => [[xsr lb] glex].
  have sd: sub (doubleton x b) (substrate r) by apply sub_doubleton.
  aw; move=> [[ysr lby] lgley].
  move: (lby _ (doubleton_first x b)) => xy.
  move: (lby _ (doubleton_second x b)) => lbyy.
  split.
    split =>// z; aw; case; last by move=> ->.
    move=>za; move: (lb _ za)=> xa; order_tac.
  move=> z [ze xx].
  apply lgley; split=>//; move=> t; rewrite doubleton_rw;case.
    move=> ->; apply glex; split=>//.
    move=> u ua; apply xx; fprops.
  move=> ->;apply xx; fprops.
by move=> Z x Zr _; aw; move=> [[xsr _] _].
Qed.

Lemma finite_subset_lattice_sup: forall r X,
  lattice r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, least_upper_bound r X x.
Proof.
move=> r X [or lr] fsX Xsr neX.
move: neX fsX Xsr.
apply finite_set_induction3.
    move=>a b asr bsr; by move: (lr _ _ asr bsr)=> [p1 p2].
  move=> a b x y asr bsr sax.
  have st: sub (tack_on a b) (substrate r) by apply tack_on_sub.
  awi sax =>//; move:sax => [[xsr lb] glex].
  have sd: sub (doubleton x b) (substrate r) by apply sub_doubleton.
  aw; move=> [[ysr lby] lgley].
  move: (lby _ (doubleton_first x b)) => xy.
  move: (lby _ (doubleton_second x b)) => lbyy.
  split.
    split =>// z; aw; case; last by move=> ->.
    move=>za; move: (lb _ za)=> xa; order_tac.
  move=> z [ze xx].
  apply lgley; split=>//; move=> t; rewrite doubleton_rw;case.
    move=> ->; apply glex; split=>//.
    move=> u ua; apply xx; fprops.
  move=> ->;apply xx; fprops.
by move=> Z x Zr _; aw; move=> [[xsr _] _].
Qed.

Lemma finite_subset_torder_greatest: forall r X,
  total_order r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, greatest_element (induced_order r X) x.
Proof.
move=>r X [or tor] fsX Xsr neX.
move: neX fsX Xsr.
apply (finite_set_induction3
  (p:=fun X x => greatest_element (induced_order r X) x)) => //.
    move=> a b asr bsr.
    have sd: sub (doubleton a b) (substrate r) by apply sub_doubleton.
    case (tor _ _ asr bsr)=> cp.
      exists b; red; aw; ee.
      move=> x; rewrite doubleton_rw; case; move=> ->; aw; fprops; order_tac.
    exists a; red; aw; ee.
    move=> x; rewrite doubleton_rw; case; move=> ->; aw; fprops; order_tac.
  move=> a b x y asr bsr;rewrite /greatest_element.
  have sta: (sub (tack_on a b) (substrate r)) by apply tack_on_sub.
  move=> [xa xp]; awi xa => //.
  move: (asr _ xa) => xsr.
  have sd: sub (doubleton x b) (substrate r) by apply sub_doubleton.
  move: xp; aw; move=> xp [yd yp]; split.
  by move: yd; case;move => ->; intuition.
  move: (yp _ (doubleton_first x b)); aw; fprops => xy.
  move: (yp _ (doubleton_second x b)); aw; fprops=> lbyy.
  have yt: inc y (tack_on a b) by aw; case yd =>->; intuition.
  move=> z zi; rewrite iorder_gle //.
  by case (tack_on_or zi) => h;
     [ move:(xp _ h); aw => zx; order_tac | rewrite h].
move=> Z x Zs neZ [h gex]; apply Zs.
move: h; aw.
Qed.

Lemma finite_subset_torder_least: forall r X,
  total_order r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, least_element (induced_order r X) x.
Proof.
move=> r X tor fsX Xsr neX.
have or: order r by move: tor=> [].
move: (total_order_opposite tor)=> rtor.
have rXsr: (sub X (substrate (opposite_order r))) by aw.
move: (finite_subset_torder_greatest rtor fsX rXsr neX)=> [x []]; aw; fprops.
move=> xX xg; exists x; split; aw=>//.
move=> a aX; move: (xg _ aX); aw.
Qed.

Lemma finite_set_torder_greatest: forall r,
  total_order r ->finite_set (substrate r) -> nonempty (substrate r)
  -> exists x, greatest_element r x.
Proof.
move=> r tor fss nes; move: (tor)=> [or _].
rewrite - (induced_order_substrate or).
apply finite_subset_torder_greatest; fprops.
Qed.

Lemma finite_set_torder_worder: forall r,
  total_order r ->finite_set (substrate r) -> worder r.
Proof.
move=> r tor fse; move: (tor)=> [or _].
split=>// z zs zne.
apply finite_subset_torder_least =>//.
apply (sub_finite_set zs fse).
Qed.

Lemma finite_set_maximal: forall r,
  order r ->finite_set (substrate r) -> nonempty (substrate r) ->
  exists x, maximal_element r x.
Proof.
move=> r or fse nes; apply Zorn_lemma=>//.
move => X Xsr toX.
case (emptyset_dichot X)=> xe.
  rewrite xe;move: nes=> [z zE]; exists z; split=>//; move=> y; case; case.
set (s:= induced_order r X) in toX.
have sr: (substrate s = X) by rewrite /s; aw.
have fs: (finite_set (substrate s)).
   by rewrite sr; apply (sub_finite_set Xsr fse).
have nse: (nonempty (substrate s)) by rewrite sr.
move: (finite_set_torder_greatest toX fs nse)=> [x [xsr xge]].
rewrite -sr in Xsr.
rewrite -sr; exists x; split; first by apply Xsr.
move=> y yX; move: (xge _ yX); rewrite /s; aw; ue.
Qed.