Library set8

Theory of Sets EIII-4 Natural integers. Finite sets

Copyright INRIA (2009) Apics Team (Jose Grimm).

Require Export set2.
Require Export set3.
Require Export set4.
Require Export set5.
Require Export set6.
Require Export set7.

Set Implicit Arguments.

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

Module FiniteSets.

EIII-4-1 Definition of integers


Definition succ x := card_plus x card_one.

Definition is_finite_c x := is_cardinal x & x <> succ x.
Definition is_finite_set x := is_finite_c (cardinal x).
Definition card_three := succ card_two.
Definition card_four := succ card_three.

Lemma integer_is_cardinal: forall x, is_finite_c x -> is_cardinal x.
Proof. ir. nin H. am. Qed.

Hint Resolve integer_is_cardinal: fprops.

Lemma cardinal_succ_pr0: forall a b, equipotent a b -> succ a = succ b.
Proof. ir. uf succ. app cardinal_sum_pr2. fprops.
Qed.

Lemma succ_is_cardinal: forall a, is_cardinal (succ a).
Proof. ir. uf succ. fprops. Qed.

Lemma cardinal_succ: forall a, cardinal (succ a) = succ a.
Proof. ir. pose (succ_is_cardinal a). fprops.
Qed.

Lemma is_finite_succ1: forall x, is_finite_c x -> is_finite_c (succ x).
Proof. ir. nin H. pose (succ_is_cardinal x). split. am. dneg.
  ap (succ_injective H i H1).
Qed.

Theorem is_finite_succ: forall x, is_cardinal x ->
  (is_finite_c x) = (is_finite_c (succ x)).
Proof. ir. ap iff_eq; ir. app is_finite_succ1. nin H0. split. am. dneg.
  wrr H2.
Qed.

Lemma succ_cardinal: forall z, succ (cardinal z) = succ z.
Proof. ir. app cardinal_succ_pr0. fprops.
Qed.

Lemma is_finite_succ2: forall x, is_finite_set x -> is_finite_c (succ x).
Proof. ir. wr (succ_cardinal x). app is_finite_succ1.
Qed.

Lemma succ_zero: succ card_zero = card_one.
Proof. ir. uf succ. aw. app cardinal1.
Qed.

Lemma is_finite0: is_finite_c card_zero.
Proof. split. ap cardinal0. rw succ_zero. red. ir. symmetry in H.
  app (card_one_not_zero).
Qed.

Lemma is_finite1: is_finite_c card_one.
Proof. wr succ_zero. app is_finite_succ1. app is_finite0.
Qed.

Lemma is_finite2: is_finite_c card_two.
Proof. rw card_two_pr. change (is_finite_c (succ card_one)).
  app is_finite_succ1. app is_finite1.
Qed.

Lemma is_finite3: is_finite_c card_three.
Proof. uf card_three. app is_finite_succ1. app is_finite2.
Qed.

Lemma is_finite4: is_finite_c card_four.
Proof. uf card_four. app is_finite_succ1. app is_finite3.
Qed.

EIII-4-2 Inequalities between integers


Lemma cardinal_le_when_complement1: forall a b,
  cardinal_le b a -> (exists c, is_cardinal c & card_plus b c = a).
Proof. ir. assert (is_cardinal a). co_tac.
  assert (is_cardinal b). co_tac.
  rwii (cardinal_le_when_complement H0 H1) H.
Qed.

Lemma is_less_than_succ: forall a, is_cardinal a ->
  cardinal_le a (succ a).
Proof. ir. uf succ. rww cardinal_le_when_complement. exists card_one.
  split. ap cardinal1. tv. fprops.
Qed.

Lemma is_finite_in_sum: forall a b, is_cardinal b ->
  is_finite_c (card_plus a b) -> is_finite_c b.
Proof. ir. split. am. nin H0. dneg. uf succ.
  wr card_plus_associative. ufi succ H2. wrr H2.
Qed.

Lemma is_finite_in_sum2: forall a b, is_cardinal a ->
  is_finite_c (card_plus a b) -> is_finite_c a.
Proof. ir. rwi card_plus_commutative H0. app (is_finite_in_sum H H0).
Qed.

Theorem le_int_is_int: forall a b, is_finite_c b ->
  cardinal_le a b -> is_finite_c a.
Proof. ir. nin (cardinal_le_when_complement1 H0). nin H1. wri H2 H.
  assert (is_cardinal a). co_tac. ap (is_finite_in_sum2 H3 H).
Qed.

Definition predc n := choose (fun m => is_cardinal m & n = succ m).

Lemma predc_pr0: forall n, is_cardinal n -> n <> card_zero ->
  (is_cardinal (predc n) & n = succ (predc n)).
Proof. ir. uf predc. app choose_pr.
  assert (cardinal_le card_one n). app one_small_cardinal.
  nin (cardinal_le_when_complement1 H1). nin H2. symmetry in H3.
  exists x. split. am. uf succ. rww card_plus_commutative.
Qed.

Lemma predc_pr: forall n, is_finite_c n -> n <> card_zero ->
  (is_finite_c (predc n) & n = succ (predc n)).
Proof. ir. assert (is_cardinal n). fprops. nin (predc_pr0 H1 H0).
  split. rww is_finite_succ. ue. am.
Qed.

Theorem exists_predc: forall n, is_finite_c n -> n <> card_zero ->
  exists_unique (fun m => is_finite_c m & n = succ m).
Proof. ir. split. exists (predc n). app predc_pr.
  ir. ee. rwi H4 H3. ap succ_injective; fprops.
Qed.

Lemma finite_in_product: forall a b, is_cardinal a -> is_cardinal b ->
  b <> card_zero -> is_finite_c (card_mult a b) -> is_finite_c a.
Proof. ir. nin (predc_pr0 H0 H1). rwi H4 H2. ufi succ H2.
  rwi cardinal_distrib_prod_sum3 H2. rwii one_unit_prodr H2.
  app (is_finite_in_sum H H2).
Qed.

Theorem lt_is_le_succ: forall a n, is_finite_c n ->
  cardinal_lt a (succ n) = cardinal_le a n.
Proof. ir. ap iff_eq. ir. nin H0.
  nin (cardinal_le_when_complement1 H0). nin H2. assert (x <> card_zero).
  red. ir. rwi H4 H3. rwi zero_unit_sumr H3. au. co_tac.
  nin (predc_pr0 H2 H4). rwi H6 H3.
  assert (card_plus a (predc x) = n). app succ_injective. fprops. fprops.
  wrr card_plus_associative. wr H7. app sum_increasing3. co_tac.
  ir. red. nin H. pose (is_less_than_succ H). ee. co_tac. dneg.
  rwi H2 H0. co_tac.
Qed.
Hint Rewrite lt_is_le_succ : sw.

Lemma is_lt_succ: forall n, is_finite_c n ->
  cardinal_lt n (succ n).
Proof. ir. rww lt_is_le_succ. fprops. Qed.

Lemma lt_is_le_succ1: forall a b, is_finite_c b ->
  cardinal_le a (succ b) -> a <> (succ b) -> cardinal_le a b.
Proof. ir. wrr lt_is_le_succ. split; am.
Qed.

Lemma lt_n_succ_le1: forall a b, is_cardinal a -> is_finite_c b ->
  cardinal_le a b = cardinal_le (succ a) (succ b).
Proof. ir. ap iff_eq. ir. uf succ. app sum_increasing2. cp cardinal1. fprops.
  ir. assert (cardinal_le a (succ a)). app is_less_than_succ.
  wrr lt_is_le_succ. split. co_tac. nin H0. dneg. wri H4 H1.
  assert (a = succ a). co_tac. wr H4. rwi H5 H4. sy. app succ_injective.
Qed.

Lemma succ_nonzero1:forall n, cardinal_le card_one (succ n).
Proof. ir. wr succ_cardinal. uf succ. rw card_plus_commutative.
  app sum_increasing3. app cardinal1. fprops.
Qed.

Lemma succ_nonzero:forall n, succ n <> card_zero.
Proof. ir. cp (succ_nonzero1 n). red. ir. rwi H0 H.
  apply zero_smallest1 with card_one. red. ee. am. ap card_one_not_zero.
Qed.

Lemma predc_pr1: forall n, is_cardinal n -> predc (succ n) = n.
Proof. ir. cp (predc_pr0 (succ_is_cardinal n) (succ_nonzero (n:=n))).
  sy. ee. app succ_injective.
Qed.

Lemma succ_positive: forall a, cardinal_lt card_zero (succ a).
Proof. ir. red. ee. app zero_smallest. app succ_is_cardinal. red. ir.
  symmetry in H. ap (succ_nonzero H).
Qed.

Lemma zero_lt_one: cardinal_lt card_zero card_one.
Proof. wr succ_zero. app succ_positive. Qed.

Lemma lt_n_succ_le0: forall a b, is_cardinal a -> is_finite_c b ->
  cardinal_le (succ a) b = cardinal_lt a b.
Proof. ir. sy. nin (equal_or_not b card_zero). rw H1.
  ap iff_eq. ir. elim (zero_smallest1 H2). ir.
  assert (cardinal_lt (succ a) card_zero). split. am. ap (succ_nonzero (n:=a)).
  elim (zero_smallest1 H3). nin (predc_pr H0 H1). rw H3.
  wrr lt_n_succ_le1. srw.
Qed.

Hint Rewrite lt_n_succ_le0 : sw.

Lemma sub_finite_set: forall x y, sub x y -> is_finite_set y ->
  is_finite_set x.
Proof. uf is_finite_set. ir. app (le_int_is_int H0 (sub_smaller H)).
Qed.

Lemma cardinal_succ_pr: forall a b, ~ (inc b a) ->
  cardinal (tack_on a b) = succ a.
Proof. ir. wr (succ_cardinal a). cp (disjoint_with_singleton H).
  uf succ. uf tack_on. assert (equipotent a (cardinal a)). fprops.
  app card_plus_pr1. uf card_one.
  eqtrans (singleton emptyset). app singletons_equipotent. fprops.
Qed.

Lemma cardinal_succ_pr1: forall a b,
  cardinal (tack_on (complement a (singleton b)) b) =
  succ (cardinal (complement a (singleton b))).
Proof. ir. rww cardinal_succ_pr. app cardinal_succ_pr0. fprops.
  app not_inc_complement_singleton.
Qed.

Lemma strict_sub_smaller: forall x y, sub x y -> is_finite_set y ->
  x<> y -> cardinal_lt (cardinal x) (cardinal y).
Proof. ir. assert (strict_sub x y). split; am.
  nin (strict_sub_nonempty_complement H2). srwi H3. nin H3.
  set (z:= complement y (singleton y0)).
  assert (sub x z). red. ir. uf z. srw. split. app H. dneg.
  wrr (singleton_eq H6).
  pose (sub_smaller H5). assert (cardinal y = succ (cardinal z)). uf z.
  wr cardinal_succ_pr1. wrr tack_on_complement. rw H6. srw.
  assert (sub z y). uf z. app sub_complement. ap (sub_finite_set H7 H0).
Qed.

Lemma emptyset_finite: is_finite_set emptyset.
Proof. red. rw cardinal_zero. app is_finite0.
Qed.

Lemma strict_sub_smaller1: forall y,
  (forall x, sub x y -> x<> y -> cardinal_lt (cardinal x) (cardinal y)) ->
  is_finite_set y.
Proof. ir. nin (emptyset_dichot y). rw H0. app emptyset_finite.
  nin H0.
  set (z:=complement y (singleton y0)). assert (sub z y). uf z.
  app sub_complement.
  assert (y = tack_on z y0). uf z. app tack_on_complement.
  cp (cardinal_succ_pr1 y y0). fold z in H3. wri H2 H3.
  assert (z <> y). red. ir. assert (inc y0 z). ue. ufi z H5. srwi H5.
  ee. elim H6. fprops. cp (H _ H1 H4). rwi H3 H5. nin H5. red.
  rw H3. wrr is_finite_succ. split; fprops. fprops.
Qed.

Lemma finite_image: forall f, is_function f -> is_finite_set (source f) ->
  is_finite_set (image_of_fun f).
Proof. ir. cp (image_smaller_cardinal H).
  red. red in H0. ap (le_int_is_int H0 H1).
Qed.

Lemma finite_image_by: forall f A, is_function f -> sub A (source f) ->
  is_finite_set A -> is_finite_set (image_by_fun f A).
Proof. ir. set (g:= restriction1 f A).
  assert (surjective g). uf g. app restriction1_surjective. nin H2.
  assert (image_of_fun g = image_by_fun f A). ue. uf g. uf restriction1. aw.
  wr H4. app finite_image. uf g. uf restriction1. aw.
Qed.

Lemma finite_fun_image: forall a f, is_finite_set a ->
  is_finite_set (fun_image a f).
Proof. ir. assert (surjective (BL f a (fun_image a f))).
  app bl_surjective. red. ir. aw. exists c. auto.
  ir. awi H0. am. nin H0. awi H1. wr H1. app finite_image. aw.
Qed.

Lemma finite_range: forall f, fgraph f -> is_finite_set(domain f) ->
  is_finite_set(range f).
Proof. ir. assert (is_function (corresp (domain f) (range f) f)).
  app is_function_pr. fprops.
  assert (range f = image_of_fun (corresp (domain f)(range f) f)).
  uf image_of_fun. aw. wrr image_by_graph_domain. fprops.
  rw H2. app finite_image. aw.
Qed.

Lemma finite_graph_domain: forall f, fgraph f ->
  is_finite_set f -> is_finite_set (domain f).
Proof. ir. uf domain. app finite_fun_image.
Qed.

Lemma finite_graph_range: forall f, fgraph f ->
  is_finite_set f -> is_finite_set (range f).
Proof. ir. uf range. app finite_fun_image.
Qed.

Lemma finite_domain_graph: forall f, fgraph f ->
  is_finite_set (domain f) -> is_finite_set f.
Proof. ir. wrr L_recovers. uf L. app finite_fun_image.
Qed.

Lemma bijective_if_same_finite_c_inj: forall f,
  cardinal (source f) = cardinal (target f) -> is_finite_set (source f) ->
  injective f -> bijective f.
Proof. ir. split. am. split. fct_tac.
  ex_middle.
  assert (sub (image_of_fun f) (target f)). nin H1. app sub_image_target.
  assert (is_finite_set (target f)). red. wr H. exact H0.
  cp (strict_sub_smaller H3 H4 H2). nin H5. elim H6.
  transitivity (cardinal (source f)). symmetry. aw. red.
  exists (restriction_to_image f). ee.
  ap (restriction_to_image_bijective H1).
  uf restriction_to_image. uf restriction2. aw.
  uf restriction_to_image. uf restriction2. aw. am.
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. ir. uf image_by_fun. uf image_of_fun. app image_by_increasing. fprops.
Qed.

Lemma bijective_if_same_finite_c_surj: forall f,
  cardinal (source f) = cardinal (target f) -> is_finite_set (source f) ->
  surjective f -> bijective f.
Proof. ir. nin (exists_right_inv_from_surj H1).
  cp (source_right_inverse H2). cp (right_inverse_injective H2).
  assert (source f = target x). nin H2. red in H2. ee; am.
  assert (cardinal (source x) = cardinal (target x)). rw H3. sy. ue.
  assert (is_finite_set (source x)). red. ue. ue.
  cp (bijective_if_same_finite_c_inj H6 H7 H4).
  nin H2. ee. assert (bijective (compose f x)). rw H9. app identity_bijective.
  app (bij_left_compose H2 H10 H8).
Qed.

EIII-6-1 The set of natural integers


Definition is_infinite_c a := is_cardinal a & ~ (is_finite_c a).
Definition infinite_set E := is_infinite_c (cardinal E).

Lemma finite_lt_infinite: forall a b,
  is_finite_c a -> is_infinite_c b -> cardinal_lt a b.
Proof. ir. nin H0. assert (is_cardinal a). fprops.
  nin (cardinal_le_total_order2 H0 H2). elim H1. ap (le_int_is_int H H3). am.
Qed.

Lemma finite_le_infinite: forall a b,
  is_finite_c a -> is_infinite_c b -> cardinal_le a b.
Proof. ir. nin (finite_lt_infinite H H0). am.
Qed.

Lemma S_inj_not_bij: injective (acreate S) & (~ surjective (acreate S)).
Proof. split. red. split. app acreate_function. aw. ir. nin H.
  nin H0. subst. rwi acreate_W H1. rwi acreate_W H1.
  cp (R_inj H1). rww (eq_add_S _ _ H).
  red. ir. assert (inc (Ro 0) (target (acreate S))). aw.
  exists 0. tv. nin (surjective_pr2 H H0). simpl in H1. ee. symmetry in H2.
  awi H1. nin H1. subst. awi H0. rwi acreate_W H2. elim (O_S x0). ap (R_inj H2).
Qed.

Lemma nat_infinite_set: is_infinite_c (cardinal nat).
Proof. red. split. fprops. red. ir.
  assert (cardinal (source (acreate S)) = cardinal (target (acreate S))). aw.
  fprops. assert (is_finite_set (source (acreate S))). aw.
  nin S_inj_not_bij.
  nin (bijective_if_same_finite_c_inj H0 H1 H2). auto.
Qed.

Definition Bnat := Zo(set_of_cardinals_le (cardinal nat))
  (fun z => is_finite_c z).

Lemma inc_Bnat: forall a, inc a Bnat = is_finite_c a.
Proof. ir. uf Bnat. ap iff_eq; ir;Ztac. am.
  assert (is_cardinal (cardinal nat)). fprops. rw (set_of_cardinals_pr a H0).
  cp nat_infinite_set. ap (finite_le_infinite H H1).
Qed.
Opaque Bnat.

Hint Rewrite inc_Bnat : bw.

Lemma inc_Bnat_prop: forall a, inc a Bnat -> is_finite_c a.
Proof. ir. bwi H. am. Qed.

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

Lemma Bnat_is_cardinal: forall x, inc x Bnat -> is_cardinal x.
Proof. ir. bwi H. nin H. am.
Qed.

Hint Resolve Bnat_is_cardinal inc_Bnat_prop : fprops.

Lemma Bnat_order_substrate: substrate Bnat_order = Bnat.
Proof. ir. assert (forall x, inc x Bnat -> is_cardinal x). ir. fprops.
  nin (wordering_cardinal_le_pr H). am.
Qed.

Lemma Bnat_order_worder: worder Bnat_order.
Proof. ir. assert (forall x, inc x Bnat -> is_cardinal x). ir. fprops.
  nin (wordering_cardinal_le_pr H). am.
Qed.

Lemma Bnat_order_le: forall x y,
  gle Bnat_order x y = Bnat_le x y.
Proof. ir. uf Bnat_order. aw. rww graph_on_rw1.
Qed.

Lemma inc0_Bnat: inc card_zero Bnat.
Proof. bw. ap is_finite0. Qed.

Lemma inc1_Bnat: inc card_one Bnat.
Proof. bw. ap is_finite1. Qed.

Lemma inc2_Bnat: inc card_two Bnat.
Proof. bw. ap is_finite2. Qed.

Lemma inc_succ_Bnat: forall x, inc x Bnat -> inc (succ x) Bnat.
Proof. ir. bw. ap is_finite_succ1. fprops. Qed.

Lemma le_int_in_Bnat: forall a b, cardinal_le a b -> inc b Bnat -> inc a Bnat.
Proof. ir. bw. bwi H0. app (le_int_is_int H0 H). Qed.

Hint Resolve inc0_Bnat inc1_Bnat inc2_Bnat inc_succ_Bnat: fprops.

Lemma predc_pr2: forall n, inc n Bnat -> predc (succ n) = n.
Proof. ir. assert (is_cardinal n). fprops. app predc_pr1.
Qed.

Lemma predc_pr3: forall n, inc n Bnat ->
  n = card_zero \/ exists m, inc m Bnat & n = succ m.
Proof. ir. nin (equal_or_not n card_zero). au. bwi H.
  nin (predc_pr H H0). right. exists (predc n). split. bw. am.
Qed.

EIII-4-3 The principle of induction


Lemma Bnat_wordered : forall X, sub X Bnat -> nonempty X ->
  inc card_zero X \/
  (exists a, inc a Bnat & inc (succ a) X & ~ (inc a X)).
Proof. ir. nin Bnat_order_worder. wri Bnat_order_substrate H. nin (H2 _ H H0).
  red in H3. awii H3. ee. rwi Bnat_order_substrate H. nin (predc_pr3 (H _ H3)).
  wr H5. au. right. nin H5. nin H5. ex_tac. wr H6. split. am. red. ir.
  cp (H4 _ H7). awii H8. rwi Bnat_order_le H8. red in H8. ee.
  bwi H5. cp (is_lt_succ H5). rwi H6 H10. co_tac.
Qed.

Lemma cardinal_c_induction_v: forall r:EP,
  (r card_zero) -> (forall n, inc n Bnat-> r n -> r (succ n))
  -> (forall n, inc n Bnat -> r n).
Proof. ir. set (X:= Zo Bnat (fun z => ~ (r z))). assert (sub X Bnat).
  uf X. app Z_sub. nin (p_or_not_p (r n)). am.
  assert (nonempty X). exists n. uf X. Ztac. nin (Bnat_wordered H2 H4).
  ufi X H5. Ztac. contradiction. nin H5. ufi X H5. ee. elim H7. Ztac.
Qed.

Lemma cardinal_c_induction: forall r:EP,
  (r card_zero) -> (forall n, is_finite_c n -> r n -> r (succ n))
  -> (forall n, is_finite_c n -> r n).
Proof. ir. assert (forall n, inc n Bnat -> r n -> r (succ n)). ir. app H0.
  fprops. app cardinal_c_induction_v. bw.
Qed.

Lemma cardinal_c_induction1: forall r:EP,
  let s:= fun n => forall p, is_finite_c n -> is_finite_c p ->
    cardinal_lt p n -> r p in
  (forall n, is_finite_c n -> s n -> r n) ->
  (forall n, is_finite_c n -> r n).
Proof. ir. app H. app cardinal_c_induction. uf s. ir.
  elim (zero_smallest1 H3). ir. red. ir. srwi H5.
  nin (equal_or_not p n0). app H. rww H6. red in H2. app H2. red. au. am.
Qed.

Lemma cardinal_c_induction2: forall (r:EP) k,
  is_finite_c k -> r k ->
  (forall n, is_finite_c n -> cardinal_le k n -> r n -> r (succ n))
  -> (forall n, is_finite_c n -> cardinal_le k n -> r n).
Proof. ir. set (s:= fun n => (cardinal_le k n -> r n)).
  assert (s n). ap cardinal_c_induction. uf s. ir.
  wrr (zero_smallest2 H4).
  ir. red. nin (equal_or_not k (succ n0)). wr H6. ir. am.
  ir. cp (lt_is_le_succ1 H4 H7 H6). app H1. app H5. am. app H4.
Qed.

Lemma cardinal_c_induction3: forall (r:EP) a b,
  is_finite_c a -> is_finite_c b -> r a ->
  (forall n, cardinal_le a n -> cardinal_lt n b -> r n -> r (succ n))
  -> (forall n, cardinal_le a n -> cardinal_le n b -> r n).
Proof. ir. set (s:= fun n => (cardinal_le a n -> cardinal_le n b -> r n)).
  assert (s n). ap cardinal_c_induction. uf s. ir.
  wrr (zero_smallest2 H5).
  red. ir. nin (equal_or_not a (succ n0)). ue.
  cp (lt_is_le_succ1 H5 H7 H9). srwi H8; tv.
  app H2. app H6. red in H8. ee. am. fprops. ap (le_int_is_int H0 H4). app H5.
Qed.

Lemma cardinal_c_induction4: forall (r:EP) a b,
  is_finite_c a -> is_finite_c b -> r b ->
  (forall n, cardinal_le a n -> cardinal_lt n b -> r (succ n) -> r n)
  -> (forall n, cardinal_le a n -> cardinal_le n b -> r n).
Proof. ir. set (q := fun n => ~ (r n)). nin (p_or_not_p (r n)). am.
  assert (is_finite_c n). app (le_int_is_int H0 H4).
  assert (forall m, cardinal_le n m -> cardinal_lt m b -> q m -> q (succ m)).
  ir. uf q. red. ir. elim H9. assert (cardinal_le a m). co_tac.
  ap (H2 _ H11 H8 H10).
  cp (cardinal_c_induction3 _ H6 H0 H5 H7). assert (q b). app H8.
  red in H0. ee. fprops. elim H9. am.
Qed.

Lemma Bnat_interval_cc_pr: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_cc Bnat_order a b) = (Bnat_le a x & Bnat_le x b).
Proof. ir. uf interval_cc. rw Bnat_order_substrate. app iff_eq. ir.
  Ztac. repeat wrr Bnat_order_le. ir. Ztac. ee.
  red in H1; ee; am. repeat rww Bnat_order_le.
Qed.

Lemma Bnat_interval_co_pr: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_co Bnat_order a b) = (Bnat_le a x & Bnat_lt x b).
Proof. ir. uf Bnat_lt. uf interval_co. rw Bnat_order_substrate. ap iff_eq. ir.
  Ztac. repeat wrr Bnat_order_le.
  ir. Ztac. ee. red in H1; ee; am. uf glt. repeat rww Bnat_order_le.
Qed.

Lemma Bnat_interval_cc_pr1: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_cc Bnat_order a b) = (cardinal_le a x & cardinal_le x b).
Proof. ir. rww Bnat_interval_cc_pr. uf Bnat_le. ap iff_eq. ir.
  intuition. ir. nin H1. set (le_int_in_Bnat H2 H0). intuition.
Qed.

Lemma Bnat_interval_co_pr1: forall a b x, inc a Bnat -> inc b Bnat ->
  inc x (interval_co Bnat_order a b) = (cardinal_le a x & cardinal_lt x b).
Proof. ir. rww Bnat_interval_co_pr. uf Bnat_lt. uf Bnat_le.
  uf cardinal_lt. ap iff_eq. ir. intuition. ir. nin H1. nin H2.
  set (le_int_in_Bnat H2 H0). intuition.
Qed.

Lemma cardinal_c_induction3_v: forall (r:EP) 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. ir. assert (forall n, cardinal_le a n -> cardinal_lt n b ->
  r n -> r (succ n)). ir. app H2. rw Bnat_interval_co_pr1. ee; am. am. am.
  rwii Bnat_interval_cc_pr1 H3. nin H3. bwi H. bwi H0.
  app (cardinal_c_induction3 r H H0).
Qed.

Lemma cardinal_c_induction4_v: forall (r:EP) 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. ir. assert (forall n, cardinal_le a n -> cardinal_lt n b ->
  r (succ n) -> r n). ir. app H2. rw Bnat_interval_co_pr1. ee; am. am. am.
  rwii Bnat_interval_cc_pr1 H3. nin H3. bwi H. bwi H0.
  app (cardinal_c_induction4 r H H0).
Qed.

Lemma tack_on_finite: forall X x,
  is_finite_set X -> is_finite_set (tack_on X x).
Proof. ir. nin (inc_or_not x X). ir. assert (tack_on X x= X).
  set_extens. rwi tack_on_inc H1. nin H1. am. rww H1. fprops. rww H1.
  ir. red. rww cardinal_succ_pr. red in H. app is_finite_succ2.
Qed.

Lemma singleton_finite: forall x, is_finite_set(singleton x).
Proof. ir. red. rw cardinal_singleton. app is_finite1.
Qed.

Lemma doubleton_finite: forall x y, is_finite_set(doubleton x y).
Proof. ir. assert (doubleton x y = tack_on (singleton x) y). set_extens.
  nin (doubleton_or H). rw H0. fprops. rw H0. fprops.
  rwi tack_on_inc H. nin H. rw (singleton_eq H). fprops. rw H. fprops. rw H.
  app tack_on_finite. ap 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. ir. nin (emptyset_dichot x). rwi H1 H0. rwi cardinal_emptyset H0.
  symmetry in H0. elim (succ_nonzero H0). nin H1.
  assert (x = tack_on (complement x (singleton y)) y). app tack_on_complement.
  exists (complement x (singleton y)). exists y. ee. am.
  app not_inc_complement_singleton. cp (cardinal_succ_pr1 x y). wri H2 H3.
  rwi H0 H3. sy. app succ_injective. fprops.
Qed.

Lemma finite_set_induction0: forall s:EP,
  s emptyset -> (forall a b, s (a) -> ~(inc b a) -> s (tack_on a b)) ->
  forall x, is_finite_set x -> s x.
Proof. ir. set (r:= fun n => forall x, cardinal x = n-> s x).
  assert (r card_zero). uf r. ir. rww (cardinal_nonemptyset H2).
  assert (forall n, is_finite_c n -> r n -> r (succ n)). ir.
  assert (is_cardinal n). fprops. red. ir.
  cp (tack_if_succ_card H5 H6). nin H7. nin H7. ee. rw H7. app H0. app H4.
  cp (cardinal_c_induction r H2 H3). cp (H4 _ H1). app H5.
Qed.

Lemma finite_set_induction: forall s:EP,
  s emptyset -> (forall a b, s (a) -> s (tack_on a b)) ->
  forall x, is_finite_set x -> s x.
Proof. ir. app (finite_set_induction0 s). ir. app H0. Qed.

Lemma finite_set_induction1: forall (A B:EP) x,
  (A emptyset -> B emptyset)
  -> (forall a b, (A a -> B a) -> A(tack_on a b) -> B(tack_on a b))
  -> is_finite_set x -> A x -> B x.
Proof. ir. set (s:= fun x => A x -> B x). app (finite_set_induction s).
Qed.

Lemma finite_set_induction2: forall (A B:EP) 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))
  -> is_finite_set x -> A x -> nonempty x -> B x.
Proof. ir. set (s:= fun x => A x -> nonempty x -> B x).
  app (finite_set_induction s). uf s. ir. nin H5. elim (emptyset_pr H5). ir.
  nin (emptyset_dichot a). assert (tack_on a b = singleton b).
  set_extens. rwi tack_on_inc H6. nin H6. rwi H5 H6. elim (emptyset_pr H6).
  rw H6. fprops. rw (singleton_eq H6). fprops. rw H6. uf s. ir. app H.
  red. ir. app H0.
Qed.

Definition set_of_finite_subsets E := Zo(powerset E)(fun X => is_finite_set X).

Definition set_of_finite_subsets_prop E F:=
  inc emptyset F & forall x X, inc x E -> inc X F -> inc (tack_on X x) F.

Lemma set_of_finite_subsets_pr: forall E,
  set_of_finite_subsets_prop E (set_of_finite_subsets E) &
  (forall F, set_of_finite_subsets_prop E F -> sub (set_of_finite_subsets E) F).
Proof. ir. split. uf set_of_finite_subsets. red. split. Ztac.
  app powerset_inc. app emptyset_sub_any. app emptyset_finite. ir. Ztac.
  clear H0. Ztac. app powerset_inc. app tack_on_sub. ap (powerset_sub H1).
  app tack_on_finite. ir. red in H. ee. red. ir.
  ufi set_of_finite_subsets H1. Ztac. set (powerset_sub H2).
  app (finite_set_induction1 (fun x=> sub x E)(fun x=> inc x F)). ir.
  app H0. app H5. fprops. app H4. app (sub_trans (a:=a) (b:= tack_on a b)).
  fprops.
Qed.

Lemma finite_union2: forall x y, is_finite_set x -> is_finite_set y ->
  is_finite_set (union2 x y).
Proof. ir. set (E:=union2 x y).
  set (t:= Zo (powerset E) (fun a=> is_finite_set (union2 x a))).
  assert(set_of_finite_subsets_prop E t). red. ee. uf t. Ztac.
  app powerset_inc. app emptyset_sub_any. assert(union2 x emptyset = x).
  set_extens. nin (union2_or H1). am. elim (emptyset_pr H2). inter2tac.
  rww H1. ir. ufi t H2. Ztac. clear H2. Ztac. uf t. Ztac. app powerset_inc.
  app tack_on_sub. ap (powerset_sub H3). uf tack_on. rw union2assoc.
  change (is_finite_set (tack_on (union2 x X) x0)). app tack_on_finite.
  nin (set_of_finite_subsets_pr E). cp (H3 _ H1). assert (inc y t). app H4.
  uf set_of_finite_subsets. Ztac. app powerset_inc. uf E. ap union2sub_second.
  ufi t H5. Ztac. am.
Qed.

Lemma finite_powerset: forall x,
  is_finite_set x -> is_finite_set (powerset x).
Proof. ir. set (t:= Zo (powerset x) (fun a=> is_finite_set (powerset a))).
  assert (set_of_finite_subsets_prop x t). red. ee. uf t. Ztac.
  app powerset_inc. app emptyset_sub_any. rw powerset_emptyset.
  app singleton_finite. ir. ufi t H1. Ztac. clear H1. uf t. Ztac.
  app powerset_inc. cp (powerset_sub H2). red. ir. rwi tack_on_inc H4. nin H4.
  app H1. rww H4. nin (inc_or_not x0 X). ir. rww (tack_on_when_inc H1).
  ir. set (w:= fun_image (powerset X) (fun t => tack_on t x0)).
  assert (equipotent (powerset X) w).
  set (f:= BL (fun t => tack_on t x0) (powerset X) w).
  assert (transf_axioms (fun t => tack_on t x0) (powerset X) w). red.
  ir. uf w. aw. exists c. ee. am. tv.
  assert (is_function f). uf f. app bl_function. exists f. ee. red. ee.
  uf f. app bl_injective. ir. set_extens.
  assert (inc x1 (tack_on u x0)). fprops. rwi H8 H10. rwi tack_on_inc H10.
  nin H10. am. rwi H10 H9. elim H1. cp (powerset_sub H6). app H11.
  assert (inc x1 (tack_on u x0)). rw H8. fprops. rwi tack_on_inc H10.
  nin H10. am. rwi H10 H9. elim H1. cp (powerset_sub H7). app H11.
  uf f. app bl_surjective. ir. ufi w H6. awi H6. nin H6. exists x1.
  ee. am. am. uf f. aw. uf f; aw.
  assert(powerset (tack_on X x0)= union2 (powerset X) w).
  set_extens. cp (powerset_sub H5). nin (inc_or_not x0 x1). ir.
  ap union2_second. uf w. aw. exists (intersection2 X x1). ee.
  app powerset_inc. app intersection2sub_first. set_extens. rwi tack_on_inc H8.
  nin H8. ap (intersection2_second H8). rww H8. nin (equal_or_not x2 x0). rw H9.
  fprops. assert (inc x2 (intersection2 X x1)). app intersection2_inc.
  cp (H6 _ H8). rwi tack_on_inc H10. nin H10. am. elim H9. ee. am. fprops. ir.
  ap union2_first. app powerset_inc. red. ir. cp (H6 _ H8). rwi tack_on_inc H9.
  nin H9. am. rwi H9 H8. elim H7. am. nin (union2_or H5).
  cp (powerset_sub H6). app powerset_inc. red. ir. assert (inc x2 X). app H7.
  fprops. ufi w H6. awi H6. nin H6. nin H6. wr H7. app powerset_inc.
  app tack_on_sub. cp (powerset_sub H6). red. ir. cp (H8 _ H9). fprops. fprops.
  rw H5. app finite_union2. red. assert (cardinal (powerset X) = cardinal w).
  aw. wr H6. am.
  cp (set_of_finite_subsets_pr x). nin H1. cp (H2 _ H0). red in H3.
  assert (inc x t). app H3. uf set_of_finite_subsets. Ztac. ap inc_x_powerset_x.
  ufi t H4. Ztac. am.
Qed.

EIII-4-4 Finite subsets of ordered sets


Lemma finite_set_induction3: forall (p:EEP) 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 -> is_finite_set X -> sub X E -> exists x, p X x.
Proof. ir. app (finite_set_induction2( fun X=> sub X E)
  (fun X => exists x, p X x)). ir. wr doubleton_singleton.
  assert (inc a E). app H5. fprops. app H. ir.
  assert (sub a E). apply sub_trans with (tack_on a b). fprops.
  am. assert (inc b E). app H7. fprops. cp (H5 H8 H6). nin H10.
  cp (H1 _ _ H8 H6 H10).
  nin (H _ _ H11 H9). exists x0. ee. app (H0 _ _ _ _ H8 H9 H10 H12).
Qed.

Lemma finite_subset_directed_bounded: forall r X,
  right_directed r ->is_finite_set X -> sub X (substrate r) -> nonempty X
  -> bounded_above r X.
Proof. ir. red.
  app (finite_set_induction3( fun X x => upper_bound r X x) (E:=(substrate r))).
  red in H. ee. ir. app H3. ir. red in H5; red in H6. ee. red. ir. ee. am.
  ir. rwi tack_on_inc H9. nin H9. apply order_transitivity with x.
  red in H; ee; am. app H8. app H7. fprops. rw H9. app H7. fprops. ir.
  red in H5. intuition.
Qed.

Lemma finite_subset_lattice_inf: forall r X,
  lattice r ->is_finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, greatest_lower_bound r X x.
Proof. ir. assert (order r). red in H; ee; am.
  app (finite_set_induction3
  (fun X x => greatest_lower_bound r X x)(E:= substrate r)). ir.
  red in H. ee. cp (H6 _ _ H4 H5). ee. nin H8. exists x. am.
  ir. rwi greatest_lower_bound_pr H6. rwi greatest_lower_bound_pr H7. ee.
  red in H6; red in H7. ee.
  rw greatest_lower_bound_pr. ee. red. ee. am. ir.
  rwi tack_on_inc H12. nin H12. apply order_transitivity with x. am. ap H10.
  fprops. app H11. rw H12. app H10. fprops. ir. ap H8. red. red in H12; ee.
  am. ir. nin (doubleton_or H14). rw H15. app H9. red. ee. am. ir.
  app H13. fprops. rw H15. app H13. fprops. am. app tack_on_sub. am.
  red. ir. nin (doubleton_or H8). rw H9. ee. red in H6; ee; am. rww H9. am.
  am. ir. red in H6. red in H6. ee. awi H6. Ztac. am. am. ap Z_sub.
Qed.

Lemma finite_subset_lattice_sup: forall r X,
  lattice r ->is_finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, least_upper_bound r X x.
Proof. ir. assert (order r). red in H; ee; am.
  app (finite_set_induction3
  (fun X x => least_upper_bound r X x)(E:= substrate r)). ir.
  red in H. ee. cp (H6 _ _ H4 H5). ee. nin H7. exists x. am.
  ir. rwi least_upper_bound_pr H6. rwi least_upper_bound_pr H7. ee.
  red in H6; red in H7. ee.
  rw least_upper_bound_pr. ee. red. ee. am. ir.
  rwi tack_on_inc H12. nin H12. apply order_transitivity with x. am. app H11.
  ap H10. fprops. rw H12. app H10. fprops. ir. ap H8. red. red in H12; ee.
  am. ir. nin (doubleton_or H14). rw H15. app H9. red. ee. am. ir.
  app H13. fprops. rw H15. app H13. fprops. am. app tack_on_sub. am.
  red. ir. nin (doubleton_or H8). rw H9. ee. red in H6; ee; am. rww H9. am.
  am. ir. red in H6. red in H6. ee. awi H6. Ztac. am. am. ap Z_sub.
Qed.

Lemma finite_subset_torder_greatest: forall r X,
  total_order r ->is_finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, greatest_element (induced_order r X) x.
Proof. ir. red in H; ee. app (finite_set_induction3
  (fun X x => greatest_element (induced_order r X) x)(E:= substrate r)).
  ir. nin (H3 _ _ H4 H5). exists b. red. aw. ee. fprops. ir. aw.
  nin (doubleton_or H7). rw H8. am. rw H8. order_tac. fprops.
  red. ir. nin (doubleton_or H7). rww H8. rww H8. exists a. red. aw. ee.
  fprops. ir. aw. nin (doubleton_or H7). rw H8. order_tac.
  rw H8. am. fprops. red. ir. nin (doubleton_or H7). rww H8. rww H8.
  uf greatest_element. intros a b x y H4 H5.
  assert (sub (tack_on a b) (substrate r)). red. ir. rwi tack_on_inc H6.
  nin H6. app H4. rww H6. ir. nin H7. awi H7; try am.
  assert (sub (doubleton x b) (substrate r)). red. ir.
  nin (doubleton_or H10). rw H11. fprops. rww H11. nin H8.
  awi H11; awi H8; try am. assert (inc y (tack_on a b)).
  nin (doubleton_or H8). rw H12. fprops. rw H12. fprops. ee. aw. awi H12. am.
  ir. aw. awi H13. nin H13.
  apw order_transitivity x. awii H9. cp (H9 _ H13). awii H14.
  assert (inc x (doubleton x b)). fprops. cp (H11 _ H14). awii H15.
  rw H13. assert (inc b (doubleton x b)). fprops. cp (H11 _ H14).
  awii H15. am. am. awii H13. awi H12. am.
  ir. red in H6. awii H6. ee. app H4.
Qed.

Lemma finite_subset_torder_least: forall r X,
  total_order r ->is_finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, least_element (induced_order r X) x.
Proof. ir. cp (total_order_opposite H).
  assert (sub X (substrate (opposite_order r))). aw. red in H; ee; am.
  nin (finite_subset_torder_greatest H3 H0 H4 H2). exists x. nin H;nin H3. ee.
  clear H7. red in H5. ee. awii H5. awii H7. red. ee.
  aw. ir. awii H8. cp (H7 _ H8). awii H9. aw.
Qed.

Lemma finite_set_torder_greatest: forall r,
  total_order r ->is_finite_set (substrate r) -> nonempty (substrate r)
  -> exists x, greatest_element r x.
Proof. ir. cp H. nin H. wr (induced_order_substrate H).
  app finite_subset_torder_greatest. fprops.
Qed.

Lemma finite_set_torder_worder: forall r,
  total_order r ->is_finite_set (substrate r) -> worder r.
Proof. ir. red. ee. red in H. ee. am. ir. app finite_subset_torder_least.
  app (sub_finite_set H1 H0).
Qed.

Lemma finite_set_maximal: forall r,
  order r ->is_finite_set (substrate r) -> nonempty (substrate r) ->
  exists x, maximal_element r x.
Proof. ir. app Zorn_lemma. red. ir.
  nin (emptyset_dichot X). nin H1. exists y. red. ee. am. ir. rwi H4 H5.
  elim (emptyset_pr H5).
  set (s:= induced_order r X). fold s in H3. assert (substrate s = X). uf s; aw.
  assert (is_finite_set (substrate s)). rw H5. app (sub_finite_set H2 H0).
  assert (nonempty (substrate s)). rww H5.
  nin (finite_set_torder_greatest H3 H6 H7). exists x. red. red in H8. nin H8.
  rwi H5 H8. ee. app H2. ir. rwi H5 H9. ufi s H9. cp (H9 _ H10). awi H11. am.
  am. am.
Qed.

EIII-4-5 Properties of finite character


Definition of_finite_character s:=
  forall x, (inc x s) = (forall y, (sub y x & is_finite_set y) -> inc y s).

Lemma of_finite_character_example: forall r, order r ->
  of_finite_character(Zo (powerset (substrate r)) (fun z =>
    total_order (induced_order r z))).
Proof. ir. red. ir. app iff_eq. ir. nin (Z_all H0). clear H0. awi H2. nin H1.
  assert (sub y (substrate r)). apw sub_trans x. Ztac. aw.
  split. fprops. aw. ir. nin H3. awi H7.
  nin (H7 _ _ (H0 _ H5) (H0 _ H6)); cp (related_induced_order1 H8).
  left. aw. right. red. aw. am. am.
  ir. assert (sub x (substrate r)). red. ir. set (y:= singleton x0).
  assert (sub y x). uf y. red. ir. rww (singleton_eq H2).
  assert (is_finite_set y). uf y. app singleton_finite.
  assert (sub y x & is_finite_set y). intuition. cp (H0 _ H4). Ztac. ee.
  cp (powerset_sub H6). app H9. uf y. fprops. Ztac. aw.
  split. fprops. aw. ir.
  set (z:= doubleton x0 y). assert(sub z x & is_finite_set z). ee.
  uf z. red. ir. nin (doubleton_or H4); rww H5.
  uf z. app doubleton_finite. cp (H0 _ H4). Ztac. nin H4.
  assert (sub z (substrate r)). apw sub_trans x.
  nin H7. awii H10.
  assert (inc x0 z). uf z. fprops. assert (inc y z). uf z. fprops.
  nin (H10 _ _ H11 H12); cp (related_induced_order1 H13). left. aw.
  right; red. aw.
Qed.

Lemma maximal_inclusion: forall s, of_finite_character s -> nonempty s ->
  exists x, maximal_element (inclusion_suborder s) x.
Proof. ir. rename H0 into Ha. assert (Hb:inc emptyset s). nin Ha. red in H.
  rwi H H0. app H0. ee. app emptyset_sub_any. app emptyset_finite.
  set (E:=union s). assert (sub s (powerset E)). red. ir.
  aw. uf E. app union_sub. app (maximal_in_powerset(A:=s) (F:=E)).
  ir. red in H. rename H2 into Hs. rw H. ir. ee.
  nin (emptyset_dichot y). rww H4. rename H4 into Hc.
  set(Zy:= fun a => choose (fun b=> inc a b & inc b So)).
  assert (forall a, inc a y -> (inc a (Zy a) & inc (Zy a) So)). ir. uf Zy.
  app choose_pr. cp (H2 _ H4). app (union_exists H5).
  set (Zz:= fun_image y Zy). assert (is_finite_set Zz). uf Zz.
  app finite_fun_image. set (r:=inclusion_suborder Zz). assert (total_order r).
  uf r; red. ee. fprops. aw. ir. assert (inc x So). ufi Zz H6. awi H6.
  nin H6. nin H6. wr H8. nin (H4 _ H6). am. assert (inc y0 So). ufi Zz H7.
  awi H7. nin H7. nin H7. wr H9. nin (H4 _ H7). am. nin (H1 _ _ H8 H9). left.
  aw. ee; am. right. red; aw. ee;am. assert (Hd:substrate r = Zz). uf r. aw.
  assert(is_finite_set (substrate r)). rww Hd.
  assert(nonempty (substrate r)). rw Hd. nin Hc. exists (Zy y0). uf Zz. aw.
  exists y0. ee. am. tv. nin (finite_set_torder_greatest H6 H7 H8).
  red in H9. nin H9. assert (sub y x). red. ir. nin (H4 _ H11).
  assert (inc (Zy x0)(substrate r)). uf r. aw. uf Zz. aw. exists x0. ee. am. tv.
  cp (H10 _ H14). ufi r H15. awi H15. ee. app H17. rwi Hd H9. ufi Zz H9. awi H9.
  nin H9. nin H9. cp (H4 _ H9). nin H13. rwi H12 H14.
  rw H. ir. ee. cp (sub_trans H15 H11). cp (Hs _ H14). rwi H H18. app H18.
  ee; am.
Qed.

Pseudo Ordinals

Definition transitive_set X:= forall x, inc x X -> sub x X.

Definition pseudo_ordinal X:= forall Y, sub Y X -> transitive_set Y ->
  Y <> X -> inc Y X.
Definition decent_set x := forall y, inc y x -> ~ (inc y y).

Lemma transitive_tack_on_itself: forall y,
  transitive_set y -> transitive_set (tack_on y y).
Proof. ir. red. ir. rwi tack_on_inc H0. nin H0. cp (H _ H0).
  red. ir. set (H1 _ H2). fprops. rw H0. red. ir. fprops.
Qed.

Lemma transitive_union: forall x, (forall y, inc y x -> transitive_set y)
  -> transitive_set (union x).
Proof. ir. red. ir. nin (union_exists H0). ee.
  cp ((H _ H2) _ H1). red. ir. set (H3 _ H4). union_tac.
Qed.

Lemma transitive_intersection: forall x, (forall y, inc y x -> transitive_set y)
  -> nonempty x -> transitive_set (intersection x).
Proof. ir. red. ir. red. ir. app intersection_inc. ir.
  app ((H _ H3) _ (intersection_forall H1 H3)).
Qed.

Lemma pseudo_ordinal_transitive1: forall x,
  pseudo_ordinal x -> (transitive_set x & decent_set x).
Proof. ir. set (y:=Zo (powerset x)(fun z=> transitive_set z & decent_set z)).
  assert (transitive_set (union y)). app transitive_union. ir. ufi y H0.
  Ztac. ee. am. assert (decent_set (union y)). red. ir. nin (union_exists H1).
  nin H2. ufi y H3. Ztac. ee. red in H6. app (H6 _ H2). red in H.
  assert (sub (union y) x). app sub_union. ir. ufi y H2. app powerset_sub.
  Ztac. am. nin (p_or_not_p (union y = x)). ir. wr H3. ee; am. ir.
  cp (H _ H2 H0 H3). assert (transitive_set (tack_on (union y) (union y))).
  app transitive_tack_on_itself.
  assert (decent_set (tack_on (union y) (union y))). red. ir.
  rwi tack_on_inc H6. nin H6. app H1. red. ir.
  assert (inc y0 (union y)). wrr H6. nin (union_exists H8). ee. ufi y H10.
  Ztac. ee. red in H13. elim (H13 _ H9). am.
  set (u:=tack_on (union y) (union y)). assert (inc u y). uf y. uf u. Ztac.
  app powerset_inc. red. ir. rwi tack_on_inc H7. nin H7. app H2. rww H7.
  red in H1. assert (sub u (union y)). app union_sub.
  set (t:= union y). assert (inc t u). uf u. rw tack_on_inc. right. tv.
  assert (inc t t). app H8. fold u in H6. nin (H6 _ H9). am.
Qed.

Lemma pseudo_ordinal_transitive: forall x,
  pseudo_ordinal x -> transitive_set x.
Proof. ir. nin (pseudo_ordinal_transitive1 H). am.
Qed.

Lemma pseudo_ordinal_tack_on: forall x,
  pseudo_ordinal x -> pseudo_ordinal (tack_on x x).
Proof. ir. red. ir. nin (inc_or_not x Y). elim H2.
  set (H1 _ H3). set_extens. rwi tack_on_inc H4.
  nin H4. app s. ue. ir. assert (sub Y x). red. ir. set (H0 _ H4).
  rwi tack_on_inc i. nin i. am. elim H3. ue.
  nin (equal_or_not Y x). rw H5. fprops. rw tack_on_inc. left. app H.
Qed.

Lemma pseudo_ordinal_emptyset: pseudo_ordinal emptyset.
Proof. red. ir. elim H1. app extensionality. ap emptyset_sub_any.
Qed.

Lemma pseudo_not_inc_itself: forall x, pseudo_ordinal x -> ~ (inc x x).
Proof. ir. cp (pseudo_ordinal_transitive1 H). ee. red in H1. red. ir.
  cp (H1 _ H2). au.
Qed.

Lemma pseudo_ordinal_dichotomy : forall x y,
  pseudo_ordinal x -> pseudo_ordinal y ->
  (inc x y \/ inc y x \/ x = y).
Proof. ir. cp (pseudo_ordinal_transitive1 H).
  cp (pseudo_ordinal_transitive1 H0).
  ee. set (z:=intersection2 x y). assert (transitive_set z).
  uf z. uf intersection2. app transitive_intersection. ir.
  nin (doubleton_or H5); ue. app nonempty_doubleton.
  assert (~ (inc z z)). red. ir. red in H4. assert (inc z (intersection2 x y)).
  am. cp (intersection2_first H7). app (H4 _ H8).
  nin (equal_or_not x y). au. assert (y <> x). intuition.
  assert (sub z x). uf z; app intersection2sub_first.
  nin (equal_or_not z x). assert (sub x y). red. ir. wri H10 H11. ufi z H11.
  ap (intersection2_second H11). cp (H0 _ H11 H1 H7). au.
  cp (H _ H9 H5 H10).
  nin (equal_or_not z y). wr H12. au.
  assert (sub z y). uf z; app intersection2sub_second.
  cp (H0 _ H13 H5 H12). assert (inc z (intersection2 x y)).
  app intersection2_inc. elim H6. am.
Qed.

Lemma pseudo_ordinal_pr: forall x, transitive_set x ->
  (forall y, inc y x -> pseudo_ordinal y) ->
  pseudo_ordinal x.
Proof. ir. red. ir. nin (emptyset_dichot (complement x Y)). elim H3.
  app extensionality. app empty_complement. nin H4.
  srwi H4. ee. cp (H0 _ H4).
  assert (sub Y y). red. ir. cp (H0 _ (H1 _ H7)).
  nin (pseudo_ordinal_dichotomy H6 H8). elim H5. app (H2 _ H7).
  nin H9. am. elim H5. rww H9. nin (equal_or_not Y y). rww H8.
  ap (H _ H4). app H6.
Qed.

Lemma pseudo_ordinal_empty: pseudo_ordinal emptyset.
Proof. red. ir. elim H1. app extensionality. app emptyset_sub_any. Qed.

Lemma inc_pseudo_pseudo: forall x y, pseudo_ordinal x -> inc y x ->
  pseudo_ordinal y.
Proof. ir. set (t:= union (Zo(powerset x) (fun y=> transitive_set y &
  forall a, inc a y -> pseudo_ordinal a))). assert (pseudo_ordinal t). red.
  app pseudo_ordinal_pr. uf t. app transitive_union. ir. Ztac. ee. am. uf t.
  ir. nin (union_exists H1). ee. Ztac. ee. app H6. assert (t=x).
  nin (pseudo_ordinal_dichotomy H H1). ufi t H2. nin (union_exists H2).
  ee. Ztac. ee. cp (powerset_sub H5). cp (H8 _ H3).
  elim (pseudo_not_inc_itself H H9). nin H2.
  cp (pseudo_ordinal_transitive H).
  set (a:= tack_on t t). assert (sub a x). uf a. red. ir. rwi tack_on_inc H4.
  nin H4. app (H3 _ H2). ue. assert (sub a t). uf t. red. ir.
  apply union_inc with a. am. Ztac. app powerset_inc. ee.
  cp (pseudo_ordinal_tack_on H1). ap (pseudo_ordinal_transitive H6).
  ir. ufi a H6. rwi tack_on_inc H6. nin H6. ufi t H6. nin (union_exists H6).
  ee. Ztac. ee. app H11. rww H6. assert (inc t a). uf a. fprops. cp (H5 _ H6).
  elim (pseudo_not_inc_itself H1 H7). sy; am.
  wri H2 H0. ufi t H0. nin (union_exists H0). ee. Ztac. ee. app H7.
Qed.

Lemma intersection_of_pseudo_ordinals: forall x, nonempty x ->
  (forall a, inc a x -> pseudo_ordinal a) -> inc (intersection x) x.
Proof. ir. set (u:= intersection x). assert (pseudo_ordinal u). uf u.
  app pseudo_ordinal_pr. app transitive_intersection. ir.
  ap pseudo_ordinal_transitive. app H0.
  ir. nin H. cp (intersection_forall H1 H). apply inc_pseudo_pseudo with y0.
  app H0. am. assert (forall a, inc a x -> sub u a). uf u. red.
  ir. app (intersection_forall H3 H2).
  assert (forall a, inc a x -> inc u a \/ a =u). ir. cp (H0 _ H3).
  nin (pseudo_ordinal_dichotomy H4 H1). cp (H2 _ H3). cp (H6 _ H5).
  elim (pseudo_not_inc_itself H4 H7). am.
  assert (exists a, inc a x & a = u). app exists_proof. red. ir.
  assert(forall a, inc a x -> inc u a). ir. cp (H4 a).
  nin (H3 _ H5). am. elim H6. ee; am.
  assert (inc u (intersection x)). app intersection_inc.
  elim (pseudo_not_inc_itself H1 H6). nin H4. ee. ue.
Qed.

Lemma worder_sub_ordinal: forall x, pseudo_ordinal x ->
  worder (inclusion_suborder x).
Proof. ir. red. ee. fprops. aw. ir. assert (inc (intersection x0) x0).
  app intersection_of_pseudo_ordinals. ir. apply inc_pseudo_pseudo with x.
  am. app H0. cp (intersection_is_least H2). set (t:= (intersection x0)) in *.
  exists t. red. aw. ee. am. nin H3. ir. aw. awi H4. ee. app H0.
  app H0. cp (H4 _ H5). awi H6. ee; am. fprops.
Qed.

Lemma pseudo_ordinal_isomorphism_unique: forall x y f,
  pseudo_ordinal x -> pseudo_ordinal y ->
  order_isomorphism f (inclusion_suborder x)(inclusion_suborder y) ->
  x = y.
Proof. ir. set (A:=Zo x(fun z => W z f <> z)). nin H1. ee. awi H4. awi H5.
  assert (Ha:is_function f). app bij_is_function.
  assert (Hb: forall a, inc a x -> inc (W a f) y). ir. rw H5. app inc_W_target.
  wrr H4.
  nin (emptyset_dichot A). assert (forall a, inc a x -> W a f = a). ir.
  ex_middle. empty_tac1 a.
  uf A. Ztac.
  set_extens. wr (H8 _ H9). app Hb. rwi H5 H9. nin H3.
  cp (surjective_pr2 H10 H9). nin H11. ee. wri H4 H11. rwi (H8 _ H11) H12. ue.
  assert (Hc:forall a b, inc a x -> inc b x -> sub a b = sub (W a f) (W b f)).
  wri H4 H6. ir. cp (H6 _ _ H8 H9). awi H10. cp (Hb _ H8). cp (Hb _ H9).
  app iff_eq. ir. assert (inc a x & inc b x & sub a b). ee; am.
  rwi H10 H14. ee; am. ir. assert (inc a x & inc b x & sub a b). rw H10.
  ee; am. ee; am.
  assert (Hd:forall a b, inc a x -> inc b x -> inc a b = inc (W a f) (W b f)).
  ir. cp (inc_pseudo_pseudo H H8). cp (inc_pseudo_pseudo H H9).
  cp (Hb _ H8). cp (Hb _ H9). cp (inc_pseudo_pseudo H0 H12).
  cp (inc_pseudo_pseudo H0 H13).
  nin (pseudo_ordinal_dichotomy H10 H11). app iff_eq. ir.
  nin (pseudo_ordinal_dichotomy H14 H15). am. nin H18.
  cp (pseudo_ordinal_transitive H14 H18). wri Hc H19. cp (H19 _ H17).
  elim (pseudo_not_inc_itself H10 H20). am. am. red in H3. ee. red in H3. ee.
  wri H4 H20. rwi (H20 _ _ H8 H9 H18) H17. elim (pseudo_not_inc_itself H11 H17).
  nin H16. cp (pseudo_ordinal_transitive H10 H16). app iff_eq. ir.
  cp (H17 _ H18). elim (pseudo_not_inc_itself H10 H19). ir.
  rwi Hc H17. cp (H17 _ H18). elim (pseudo_not_inc_itself H14 H19). am. am.
  rw H16. app iff_eq. ir. elim (pseudo_not_inc_itself H11 H17). ir.
  elim (pseudo_not_inc_itself H15 H17).

  assert (sub A x). uf A. app Z_sub.
  cp (worder_sub_ordinal H). nin H9. ee. awi H10. cp (H10 _ H8 H7). nin H11.
  red in H11. nin H11. awi H11. awi H12.
  assert (forall x1, inc x1 A -> sub x0 x1). ir. cp (H12 _ H13). awi H14. ee.
  am. am. am. clear H10; clear H12.
  assert (forall u, inc u x0 -> W u f= u). ir. ex_middle.
  assert (inc u x). assert (inc x0 x). app H8.
  cp (pseudo_ordinal_transitive H). red in H15. app (H15 _ H14).
  assert (inc u A). uf A. Ztac. cp (inc_pseudo_pseudo H H14).
  cp (H13 _ H15). cp (H17 _ H10). elim (pseudo_not_inc_itself H16 H18).
  assert(forall u b, inc b x -> inc u (W b f) -> exists v, inc v b & u =W v f).
  ir. red in H3. ee. cp (Hb _ H12). cp (pseudo_ordinal_transitive H0 H16).
  cp (H17 _ H14). rwi H5 H18. cp (surjective_pr2 H15 H18). nin H19. nin H19.
  symmetry in H20. rwi H20 H14. wri Hd H14. exists x1. ee; am. rww H4. am.
  assert (sub (W x0 f) x0). red. ir. cp (H12 _ _ (H8 _ H11) H14). nin H15.
  nin H15. rw H16. rww H10. cp (inc_pseudo_pseudo H (H8 _ H11)).
  cp (inc_pseudo_pseudo H0 (Hb _ (H8 _ H11))).
  assert (He:W x0 f <> x0). ufi A H11. Ztac. am.
  nin (pseudo_ordinal_dichotomy H15 H16).
  elim (pseudo_not_inc_itself H15 (H14 _ H17)). nin H17. cp (H10 _ H17).
  red in H3. ee; red in H3. ee. wri H4 H20.
  cp (H8 _ H11). cp ( (pseudo_ordinal_transitive H H21) _ H17).
  elim He. app H20. elim He. sy; am. am. aw. am. aw.
Qed.

Lemma pseudo_ordinal_isomorphism_exists: forall r, worder r ->
  exists y, exists f, (pseudo_ordinal y &
  order_isomorphism f r (inclusion_suborder y)).
Proof. ir. set (p:= fun f => target f). cp (transfinite_definition p H).
  nin H0. clear H1. nin H0. rename x into f. red in H0. ee. ufi p H2.
  exists (target f). exists f.
  set (todo:= pseudo_ordinal (target f) &
  order_isomorphism f r (inclusion_suborder (target f))).
  set (E:= substrate r). fold E in H2. fold E in H1.
  assert (Ha: is_function f). red in H0; ee; am.
  assert (forall a b, gle r a b -> sub (W a f) (W b f)). ir.
  assert (inc a E). uf E. order_tac.
  assert (inc b E). uf E. order_tac. rww H2. rww H2.
  uf restriction_to_segment. uf restriction1. aw.
  uf image_by_fun. app image_by_increasing. fprops.
  app segment_monotone. red in H; ee;am.
  assert (forall a b, glt r a b -> inc (W a f) (W b f)). ir.
  assert (inc b E). uf E. order_tac. rw (H2 _ H5).
  uf restriction_to_segment. uf restriction1. aw.
  exists a. ee. app segment_inc. tv. rw H1. uf E. app sub_segment.
  assert(He:forall a b, inc a E -> inc b (W a f) -> sub b (W a f)).
  red. ir. rwi (H2 _ H5) H6. ufi restriction_to_segment H6.
  ufi restriction1 H6. awi H6. nin H6. nin H6.
  cp (inc_segment H6). red in H9. ee. cp (H3 _ _ H9). app H11. ue. fprops.
  rw H1. uf segment. uf interval_uo. app Z_sub.
  assert (forall a, inc a E -> ~ (inc (W a f) (W a f))).
  set (Bad:= Zo E (fun a => inc (W a f) (W a f))). nin (emptyset_dichot Bad).
  ir. red. ir. empty_tac1 a. uf Bad. Ztac.
  red in H. ee. fold E in H6. assert (sub Bad E).
  uf Bad. app Z_sub. nin (H6 _ H7 H5). red in H8. ee. awi H8. awi H9.
  cp H8. ufi Bad H8. Ztac. clear H8. set (w:= W x f). assert (inc w (W x f)).
  tv. rwi (H2 _ H11) H8. ufi restriction_to_segment H8.
  ufi restriction1 H8. awi H8. nin H8. nin H8.
  cp (inc_segment H8). assert (inc x0 (source f)). rw H1. uf E. order_tac.
  assert (inc x0 Bad). uf Bad. Ztac. wrr H1. rww H13. cp (H9 _ H16).
  awi H17. order_tac. am. am. am. rw H1. uf E. app sub_segment. am. am. am. am.
  assert (injective f). red. ee. red in H0. ee. am. ir. rwi H1 H6; rwi H1 H7.
  cp (worder_total H). cp (total_order_pr1 H9 H6 H7). nin H10.
  cp (H4 _ _ H10). rwi H8 H11. elim (H5 _ H7). am. nin H10.
  assert (glt r y x). red in H10; ee. red in H10. red. ee. am. intuition.
  cp (H4 _ _ H11). rwi H8 H12. elim (H5 _ H7). am. am.
  assert (order_isomorphism f r (inclusion_suborder (target f))). red. ee.
  red in H. ee. am. fprops. red. ee;am. rww H1. aw. ir. aw. app iff_eq. ir.
  ee. app inc_W_target. app inc_W_target. app H3. ir. ee.
  cp (worder_total H). rwi H1 H7; rwi H1 H8. cp (total_order_pr1 H12 H7 H8).
  nin H13. red in H13; ee; am. nin H13. red in H13. ee. red in H13.
  cp (H3 _ _ H13). assert ( (W y f)= (W x f)). app extensionality.
  elim H14. red in H6. ee. app H17. rww H1. rww H1. sy; am. rw H13.
  wrr order_reflexivity. red in H; ee;am.
  assert (forall a, inc a E -> transitive_set (W a f)). ir. red. ir. app He.
  assert (forall a, inc a E -> pseudo_ordinal (W a f)).
  set (Bad:= Zo E (fun z => (~ (pseudo_ordinal (W z f))))).
  nin (emptyset_dichot Bad). ir. nin (p_or_not_p (pseudo_ordinal (W a f))).
  am. assert (inc a emptyset). wr H9. uf Bad. Ztac. elim (emptyset_pr H12).
  red in H. ee. assert (sub Bad E). uf Bad. app Z_sub. cp (H10 _ H11 H9).
  nin H12. red in H12. ee. awi H12. awi H13.
  assert (Hd: inc x Bad). am. ufi Bad H12. Ztac. clear H12. elim H15.
  app pseudo_ordinal_pr. app H8. ir. rwi (H2 _ H14) H12. simpl in H12.
  ufi image_by_fun H12. ufi restriction_to_segment H12. ufi restriction1 H12.
  awi H12. nin H12. nin H12. cp (inc_segment H12). wr H16.
  nin (p_or_not_p (pseudo_ordinal (W x0 f))). am.
  assert (inc x0 Bad). uf Bad. Ztac. uf E. order_tac.
  cp (H13 _ H19). awi H20. order_tac. am. am. am. rw H1. uf E. app sub_segment.
  am. am. am. am.
  assert (transitive_set (target f)). red. ee. ir. cp (surjective_pr2 H0 H10).
  nin H11. ee. red. ir. rwi H1 H11. cp (H2 _ H11).
  ufi restriction_to_segment H14. ufi restriction1 H14. awi H14.
  wri H12 H13.
  rwi H14 H13. ufi image_by_fun H13. awi H13. nin H13. nin H13.
  graph_tac. red. ee.
  app pseudo_ordinal_pr. ir. cp (surjective_pr2 H0 H11). nin H12. nin H12.
  wr H13. app H9. wrr H1. am.
Qed.

Lemma pseudo_ordinal_pr1: forall x, exists y,
  pseudo_ordinal y & equipotent x y &
  (forall z, pseudo_ordinal z -> equipotent x z -> sub y z).
Proof. ir. nin (Zermelo x). nin H.
  destruct (pseudo_ordinal_isomorphism_exists H) as [u [f [H1 H2]]].
  assert (equipotent x u). red in H2. ee. awi H6. rwi H0 H5. exists f. ee. am.
  sy; am. sy; am. set (t:=Zo u (fun z=> equipotent x z)).
  nin (emptyset_dichot t). exists u. ee. am. am. ir.
  nin (pseudo_ordinal_dichotomy H1 H5).
  cp (pseudo_ordinal_transitive H5). red in H8. app H8. nin H7.
  empty_tac1 z. uf t. Ztac. rw H7.
  fprops. assert (sub t u). uf t. app Z_sub. cp (worder_sub_ordinal H1).
  red in H6. ee. awi H7. cp (H7 _ H5 H4). nin H8. nin H8. awi H8.
  cp H8. ufi t H8. Ztac. clear H8. cp (inc_pseudo_pseudo H1 H11). exists x1.
  ee. am. am. ir. nin (pseudo_ordinal_dichotomy H1 H13). red. ir.
  cp (pseudo_ordinal_transitive H13). red in H17. cp(H17 _ H15). app H18.
  cp (pseudo_ordinal_transitive H1). red in H19. cp(H19 _ H11). app H20.
  nin H15. assert (inc z t). uf t. Ztac. awi H9. cp (H9 _ H16). awi H17.
  ee; am. am. am. fprops. aw. wr H15. cp (pseudo_ordinal_transitive H1).
  red in H16. app H16. fprops. aw.
Qed.
Link between pseudo-ordinal and nat

Fixpoint natR (n:nat) :=
  match n with 0 => emptyset | S p => tack_on (natR p) (natR p) end.

Lemma value_R_0: natR 0 = emptyset.
Proof. tv. Qed.

Lemma value_R_1: natR 1 = singleton emptyset.
Proof. simpl. set_extens. rwi tack_on_inc H. nin H.
  elim (emptyset_pr H). rw H. fprops. rw (singleton_eq H). fprops.
Qed.

Lemma value_R_2: natR 2 = doubleton (singleton emptyset) emptyset.
Proof. simpl. cp value_R_1. simpl in H. rw H. set_extens. rwi tack_on_inc H0.
  nin H0. rw (singleton_eq H0). fprops. rw H0. fprops.
  nin (doubleton_or H0). rw H1. fprops. rw H1. fprops.
Qed.

Lemma value_R_3: let tripleton a b c := tack_on (doubleton a b) c in
  natR 3 = tripleton (doubleton (singleton emptyset) emptyset)
  (singleton emptyset) emptyset.
Proof. simpl. cp value_R_2. simpl in H. rw H. set_extens.
  rwi tack_on_inc H0. nin H0. nin (doubleton_or H0). rw H1. fprops. rw H1.
  fprops. rw H0. fprops. rwi tack_on_inc H0. nin H0. nin (doubleton_or H0).
  rw H1. fprops. rw H1. fprops. rw H0. fprops.
Qed.

Lemma pseudo_ordinal_Rnat: forall i, pseudo_ordinal (natR i).
Proof. ir. nin i. simpl. app pseudo_ordinal_emptyset. simpl.
  app pseudo_ordinal_tack_on.
Qed.

Lemma finite_Rnat: forall i, is_finite_set (natR i).
Proof. ir. nin i. simpl. app emptyset_finite. simpl. app tack_on_finite.
Qed.

Lemma Rnat_le_implies_sub : forall i j, i <= j -> sub (natR i) (natR j).
Proof. ir. nin H. fprops. apply sub_trans with (natR m). am. red. ir.
  simpl. fprops.
Qed.

Lemma Rnat_lt_implies_inc : forall i j, i < j -> inc (natR i) (natR j).
Proof. ir. red in H. cp (Rnat_le_implies_sub H). app H0. simpl. fprops.
Qed.

Lemma Rnat_lt_implies_strict_sub : forall i j,
  i < j -> strict_sub (natR i) (natR j).
Proof. ir. cp (Rnat_lt_implies_inc H). cp (pseudo_ordinal_Rnat j). red.
  ee. red. ir. rwi H2 H0. ap (pseudo_not_inc_itself H1). am.
  app pseudo_ordinal_transitive.
Qed.

Lemma Rnat_sub_le : forall i j, sub (natR i) (natR j) = (i <= j).
Proof. ir. ap iff_eq; ir. cp (le_or_lt i j). nin H0. am.
  cp (Rnat_lt_implies_inc H0). cp (H _ H1).
  elim (pseudo_not_inc_itself (pseudo_ordinal_Rnat j)). am.
  app Rnat_le_implies_sub.
Qed.

Lemma Rnot_inc_itself:forall i, ~ (inc (natR i)(natR i)).
Proof. ir. ap (pseudo_not_inc_itself (pseudo_ordinal_Rnat i)).
Qed.

Lemma Rnat_inc_lt : forall i j, inc (natR i) (natR j) = (i < j).
Proof. ir. ap iff_eq; ir. nin (le_or_lt j i). cp (Rnat_le_implies_sub H0).
  elim (Rnot_inc_itself _ (H1 _ H)). am. app Rnat_lt_implies_inc.
Qed.

Lemma cardinal_Rnat_lt: forall i j,
  i< j -> cardinal_lt (cardinal (natR i)) (cardinal (natR j)).
Proof. ir. cp (Rnat_lt_implies_strict_sub H). nin H0. app strict_sub_smaller.
  app (finite_Rnat j).
Qed.

Lemma cardinal_Rnat_inj: forall i j,
  cardinal (natR i) = cardinal (natR j) -> i = j.
Proof. ir. nin (p_or_not_p (i = j)). am. nin (nat_total_order _ _ H0).
  cp (cardinal_Rnat_lt H1). red in H2. ee. elim H3. am.
  cp (cardinal_Rnat_lt H1). red in H2. ee. elim H3. sy; am.
Qed.

Lemma exists_nat_cardinal: forall a, is_finite_c a ->
  exists_unique(fun i => cardinal (natR i) = a).
Proof. ir. red. split.
  app (cardinal_c_induction (fun n => exists i:nat, cardinal (natR i) =n)).
  exists 0. simpl. rw cardinal_zero. tv. ir. nin H1. exists (S x). simpl.
  wr H1. rw succ_cardinal. app cardinal_succ_pr. ap Rnot_inc_itself.
  ir. wri H1 H0. app cardinal_Rnat_inj.
Qed.

Definition cardinal_nat x :=
  choosenat(fun i => cardinal (natR i) = cardinal x).

Lemma cardinal_nat_cardinal: forall x,
  cardinal_nat (cardinal x) = cardinal_nat x.
Proof. uf cardinal_nat. ir.
  set (t := cardinal x). assert (is_cardinal t). uf t. fprops.
  rww (cardinal_of_cardinal H).
Qed.

Hint Rewrite cardinal_nat_cardinal: aw.

Lemma cardinal_nat_pr: forall x, is_finite_set x ->
  cardinal (natR (cardinal_nat x)) = cardinal x.
Proof. ir. uf cardinal_nat. ap choosenat_pr. nin (exists_nat_cardinal H). am.
Qed.

Lemma cardinal_nat_pr1: forall i, cardinal_nat(natR i) = i.
Proof. ir. cp (finite_Rnat i). cp (cardinal_nat_pr H).
  app cardinal_Rnat_inj.
Qed.

Lemma cardinal_nat_finite_eq: forall a b, is_finite_set a ->
  cardinal a = cardinal b -> cardinal_nat a = cardinal_nat b.
Proof. ir. assert (is_finite_set b). red. ue.
  wri (cardinal_nat_pr H) H0. wri(cardinal_nat_pr H1) H0. app cardinal_Rnat_inj.
Qed.

Lemma cardinal_nat_finite_eq1: forall a b, is_finite_set a -> is_finite_set b ->
  cardinal_nat a = cardinal_nat b -> cardinal a = cardinal b.
Proof. ir. wr (cardinal_nat_pr H). wr (cardinal_nat_pr H0). ue.
Qed.

Lemma cardinal_nat_emptyset: cardinal_nat emptyset = 0.
Proof. ir. change(cardinal_nat (natR 0) = 0). ap cardinal_nat_pr1.
Qed.

Lemma cardinal_nat_singleton: forall x, cardinal_nat (singleton x) = 1.
Proof. ir. wr (cardinal_nat_pr1 1). rw value_R_1. app cardinal_nat_finite_eq.
  app singleton_finite. aw. app singletons_equipotent.
Qed.

Lemma cardinal_nat_doubleton: forall x y,
  x <> y -> cardinal_nat (doubleton x y) = 2.
Proof. ir. wr (cardinal_nat_pr1 2). rw value_R_2. app cardinal_nat_finite_eq.
  app doubleton_finite. aw. ap doubleton_equipotent1. am. fprops.
Qed.

Lemma cardinal_nat_zero: cardinal_nat card_zero = 0.
Proof. ir. rw zero_is_emptyset. app cardinal_nat_emptyset.
Qed.

Lemma cardinal_nat_one: cardinal_nat card_one = 1.
Proof. ir. cp cardinal_one_is_singleton. nin H. rw H.
  app cardinal_nat_singleton.
Qed.

Lemma cardinal_nat_two: cardinal_nat card_two = 2.
Proof. ir. uf card_two. cp (two_points_distinct).
  wr (cardinal_nat_doubleton H). aw. rww two_points_pr2.
Qed.
Bijection between nat and the integers

Lemma plus_via_succ: forall a n,
  card_plus a (succ n) = succ (card_plus a n).
Proof. ir. uf succ. app card_plus_associative.
Qed.

Lemma Bnat_stable_plus: forall a b, inc a Bnat -> inc b Bnat ->
  inc (card_plus a b) Bnat.
Proof. ir. bw. bwi H. bwi H0.
  app (cardinal_c_induction (fun b => is_finite_c (card_plus a b))).
  aw. fprops. ir. rw plus_via_succ. app is_finite_succ1.
Qed.

Lemma mult_via_plus: forall a b, is_cardinal a ->
  card_mult a (succ b) = card_plus (card_mult a b) a.
Proof. ir. uf succ. rw cardinal_distrib_prod_sum3. aw.
Qed.

Lemma Bnat_stable_mult: forall a b, inc a Bnat -> inc b Bnat ->
  inc (card_mult a b) Bnat.
Proof. ir. app (cardinal_c_induction_v (fun b => inc (card_mult a b) Bnat)).
  aw. rw zero_prod_absorbing. fprops. ir. rw mult_via_plus.
  app Bnat_stable_plus. fprops.
Qed.

Hint Resolve Bnat_stable_plus Bnat_stable_mult: fprops.
Hint Rewrite succ_zero:aw.

Fixpoint nat_to_B (n:nat) :=
  match n with 0 => card_zero | S m => succ (nat_to_B m) end.

Lemma nat_B_0: nat_to_B 0 = card_zero.
Proof. tv. Qed.

Lemma nat_B_1: nat_to_B 1 = card_one.
Proof. simpl. aw.
Qed.

Lemma nat_B_S: forall n, nat_to_B (S n) = succ (nat_to_B n).
Proof. tv.
Qed.

Lemma inc_nat_to_B: forall n, inc (nat_to_B n) Bnat.
Proof. ir. induction n. simpl. fprops. simpl. fprops.
Qed.

Hint Resolve inc_nat_to_B: fprops.

Lemma nat_B_plus: forall a b,
  nat_to_B (a+b) = card_plus (nat_to_B a) (nat_to_B b).
Proof. ir. induction b. rw plus_0_r. sy. app zero_unit_sumr.
  cp (inc_nat_to_B a). fprops. assert (a+ S b = S(a+b)). auto with arith.
  rw H. rw nat_B_S. rw IHb. rw nat_B_S. uf succ. rww card_plus_associative.
Qed.

Lemma nat_B_2: nat_to_B 2 = card_two.
Proof. rw card_two_pr. wr nat_B_1. wrr nat_B_plus.
Qed.

Lemma nat_B_mult: forall a b,
  nat_to_B (a*b) = card_mult (nat_to_B a) (nat_to_B b).
Proof. ir. induction b. rw mult_0_r. rw nat_B_0. sy. ap zero_prod_absorbing.
  assert (a* S b = a*b+a). auto with arith. rw H. rw nat_B_plus.
  rw IHb. rw nat_B_S. uf succ. rw cardinal_distrib_prod_sum3.
  rww one_unit_prodr. cp (inc_nat_to_B a). fprops.
Qed.

Lemma nat_to_B_surjective: forall n, inc n Bnat -> exists m,
  nat_to_B m = n.
Proof. ir. app (cardinal_c_induction_v (fun b => exists m, nat_to_B m = b)).
  ir. exists 0. ap nat_B_0. ir. nin H1. exists (S x). wr H1. ap nat_B_S.
Qed.

Lemma nat_B_inj: forall a b,
  nat_to_B a = nat_to_B b -> a = b.
Proof. intro a. induction a. ir. rwi nat_B_0 H. induction b. tv. rwi nat_B_S H.
  cp (succ_positive (nat_to_B b)). red in H0. ee. elim H1. am.
  ir. induction b. rwi nat_B_S H. rwi nat_B_0 H.
  cp (succ_positive (nat_to_B a)). red in H0. ee. elim H1. sy;am.
  rwi nat_B_S H. rwi nat_B_S H. assert (a=b). app IHa. app succ_injective.
  cp (inc_nat_to_B a). fprops. cp (inc_nat_to_B b). fprops. rww H0.
Qed.

Lemma nat_B_le: forall a b,
  (a<= b) = cardinal_le (nat_to_B a) (nat_to_B b).
Proof. ir. app iff_eq. ir. cp (inc_nat_to_B a). induction H. fprops.
  apply cardinal_le_transitive with (nat_to_B m). am.
  rw nat_B_S. app is_less_than_succ. cp (inc_nat_to_B m). fprops.
  ir. cp (inc_nat_to_B a). cp (inc_nat_to_B b).
  assert (is_cardinal (nat_to_B a)). fprops.
  assert (is_cardinal (nat_to_B b)). fprops.
  rwi (cardinal_le_when_complement H3 H2) H. nin H. ee.
  bwi H1. wri H4 H1. cp (is_finite_in_sum H H1). wri inc_Bnat H5.
  nin (nat_to_B_surjective H5). wri H6 H4. wri nat_B_plus H4.
  cp (nat_B_inj _ _ H4). wr H7. auto with arith.
Qed.

Lemma nat_B_lt: forall a b,
  (a< b) = cardinal_lt (nat_to_B a) (nat_to_B b).
Proof. ir. app iff_eq. ir. red. ee. wr nat_B_le. app lt_le_weak. red. ir.
  rwi (nat_B_inj _ _ H0) H. elim (lt_irrefl _ H). ir.
  nin H. wri nat_B_le H. nin (le_lt_or_eq _ _ H). am. elim H0. ue.
Qed.

Lemma nat_B_lt0: forall b,
  (0<b) = cardinal_lt card_zero (nat_to_B b).
Proof. ir. wr nat_B_0. wr nat_B_lt. tv.
Qed.

Lemma nat_B_lt1: forall b,
  (1<b) = cardinal_lt card_one (nat_to_B b).
Proof. ir. wr nat_B_1. wr nat_B_lt. tv.
Qed.

Lemma nat_to_B_pr: forall n, inc n Bnat ->
  nat_to_B (cardinal_nat n) = n.
Proof. ir.
  app (cardinal_c_induction_v (fun b => nat_to_B (cardinal_nat b) = b)).
  rw cardinal_nat_zero. app nat_B_0. ir.
  assert (cardinal_nat (succ n0) = S (cardinal_nat n0)).
  wr (cardinal_nat_pr1 (S (cardinal_nat n0))).
  assert (is_finite_set (succ n0)). red. rw cardinal_succ. wr inc_Bnat. fprops.
  app cardinal_nat_finite_eq. awi H0. assert (cardinal n0 = n0).
  red in H0; ee. fprops. assert (is_finite_set n0). red. rw H3. bwi H0. am.
  cp (cardinal_nat_pr H4). rw cardinal_succ. simpl. fprops.
  rw cardinal_succ_pr. set (m:= cardinal_nat n0) in *.
  wr H3. wr H5. rw succ_cardinal. tv. app Rnot_inc_itself.
  rw H2. rw nat_B_S. ue.
Qed.

Lemma nat_to_B_pr1: forall n,
  cardinal_nat(nat_to_B n) = n.
Proof. ir. app nat_B_inj. rww nat_to_B_pr. fprops.
Qed.

Hint Rewrite nat_to_B_pr nat_to_B_pr1: aw.

Hint Rewrite <- nat_B_lt nat_B_le nat_B_S nat_B_lt0 nat_B_plus nat_B_mult :bw.
Hint Rewrite nat_B_lt nat_B_S nat_B_lt0 nat_B_plus nat_B_mult :aw.

Fixpoint pow (n m:nat) {struct m} : nat :=
  match m with
  | O => 1
  | S p => (pow n p) * n
  end
where "n ^ m" := (pow n m) : nat_scope.

End FiniteSets.
Export FiniteSets.