Library sset8

Theory of Sets EIII-4 Natural integers. Finite sets

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset7.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module CardinalOps.

EIII-3-3 Operations on Cardinals

Definition card_sum x := cardinal (disjointU x).
Definition card_prod x := cardinal (productb x).
Definition card_sumb a f := card_sum (Lg a f).
Definition card_prodb a f := card_prod (Lg a f).

Lemma card_sum_gr f: card_sum (Lg (domain f) (Vg f)) = card_sum f.
Proof.
congr cardinal; rewrite /disjointU /disjointU_fam; bw.
apply: f_equal; apply:Lg_exten => x xdf; bw.
Qed.

Lemma card_prod_gr f: card_prodb (domain f) (Vg f) = card_prod f.
Proof.
by rewrite /card_prodb/card_prod; congr cardinal; apply: @productb_gr.
Qed.

Lemma csumb_exten A f g : {inc A , f =1 g } -> card_sumb A f = card_sumb A g.
Proof. by move => h; congr card_sum; apply: Lg_exten. Qed.

Lemma cprodb_exten A f g : {inc A , f =1 g } -> card_prodb A f = card_prodb A g.
Proof. by move => h; congr card_prod; apply: Lg_exten. Qed.

Theorem cprod_pr x:
  cardinal (productb x) =
  card_prodb (domain x) (fun a => cardinal (Vg x a)).
Proof.
rewrite - /(card_prod x) - card_prod_gr; apply /card_eqP.
apply: equipotent_setXb; split; fprops; bw => i idx; bw; fprops.
Qed.

Theorem csum_pr x:
  cardinal (disjointU x) =
  card_sumb (domain x) (fun a => cardinal (Vg x a)).
Proof.
rewrite - /(card_sum x) - card_sum_gr; apply /card_eqP.
apply: equipotent_disjointU1;split;fprops; bw => i idx;bw;fprops.
Qed.

Lemma csum_pr3 X Y:
  domain X = domain Y ->
  (forall i, inc i (domain X) -> cardinal (Vg X i) = cardinal (Vg Y i)) ->
  card_sum X = card_sum Y.
Proof.
by move=> dXY sc; rewrite /card_sum 2!csum_pr -dXY; apply:csumb_exten.
Qed.

Lemma csum_pr4 X:
   mutually_disjoint X ->
   cardinal (unionb X) = card_sumb (domain X) (fun a => cardinal (Vg X a)).
Proof.
move => pa; rewrite - csum_pr; apply /card_eqP.
apply: equipotent_disjointU => //; last by exact (@disjointU_disjoint X).
rewrite /disjointU_fam; split; fprops; bw => i idx; bw; fprops.
Qed.

Lemma csum_pr4_bis X f:
  (forall i j, inc i X -> inc j X -> i = j \/ disjoint (f i) (f j)) ->
  cardinal (unionf X f) = card_sumb X (fun a => cardinal (f a)).
Proof.
set x := Lg X f => h.
have h1: mutually_disjoint x.
  by rewrite /x;hnf; bw => i j iX jX; bw; apply:h.
have ->: unionf X f = unionb x.
  rewrite/unionb/x; bw; apply:setUf_exten => t tX; bw.
have ->: card_sumb X (fun a => cardinal (f a)) =
    card_sumb (domain x) (fun a => cardinal (Vg x a)).
  rewrite /card_sumb /x; bw; congr cardinal; congr disjointU.
  apply:Lg_exten => t tX; bw.
apply:(csum_pr4 h1).
Qed.

Lemma csum_pr1 x:
  cardinal (unionb x) <=c card_sumb (domain x) (fun a => cardinal (Vg x a)).
Proof.
rewrite - (csum_pr x);apply: surjective_cardinal_le.
move: (disjointU_pr x) => /=; set f := common_ext _ _ _.
by move => [sf tg srfj _]; exists f.
Qed.

Lemma csum_pr1_bis X f:
  cardinal (unionf X f) <=c card_sumb X (fun a => cardinal (f a)).
Proof.
set x := Lg X f.
have ->: unionf X f = unionb x.
  rewrite/unionb/x; bw; apply:setUf_exten => t tX; bw.
have ->: card_sumb X (fun a => cardinal (f a)) =
    card_sumb (domain x) (fun a => cardinal (Vg x a)).
  rewrite /card_sumb /x; bw; congr cardinal; congr disjointU.
  apply:Lg_exten => t tX; bw.
apply:(csum_pr1 x).
Qed.

Theorem csum_Cn X f:
  target f = domain X -> bijection f ->
  card_sum X = card_sum (X \cf (graph f )).
Proof.
move=> tf [[ff injf] sjf].
have sf:source f = domain (graph f) by aw.
set X' := Lg (domain X) (Vg X).
have aux : (Lg (source f) (fun z => Vg X (Vf f z))) = X' \cf (graph f).
  rewrite /composef -(proj33 ff); apply: Lg_exten => i idf; rewrite /X';bw.
  rewrite -tf -/(Vf _ _); Wtac.
have aux2: (Lg (source f) (fun z : Set => Vg X (Vf f z))) = X \cf (graph f).
  rewrite /composef -(proj33 ff); apply: Lg_exten => i idf; rewrite /X';bw.
rewrite -aux2 aux.
have ->: card_sum X = card_sum X' by rewrite /X' card_sum_gr.
pose g:= Lg (source f) (fun i => (Vg (X' \cf (graph f)) i ) *s1 (Vf f i )).
apply /card_eqP; eqtrans (unionb g); last first.
  rewrite /g - aux ;apply: equipotent_disjointU;
  first (rewrite /disjointU_fam; bw; red;bw;split => // i isf; bw; fprops; ue);
  apply: mutually_disjoint_prop2; bw => i j y isf jsf; bw;
   move /setX_P => [_ _ /set1_P e1] /setX_P [_ _ /set1_P e2];
rewrite e1 // in e2; apply: (injf _ _ isf jsf e2).
rewrite/card_sum /disjointU/ disjointU_fam; aw.
set h := Lg _ _.
have ->: (g = h \cf (graph f)).
  rewrite /h/g; apply: fgraph_exten; fprops;bw;rewrite ? composef_domain //.
  by move=> x xsf /=; bw; try ue;rewrite /X' -tf -/ (Vf f x); bw; Wtac.
rewrite - setUb_rewrite1 /h //; bw; fprops.
rewrite (surjective_pr3 sjf) tf /X'; bw.
Qed.

Lemma csum_Cn' X f: bijection f ->
  card_sumb (target f) X = card_sumb (source f) (fun i => (X (Vf f i))).
Proof.
move => bf; rewrite /card_sumb.
have ff: function f by fct_tac.
have h: target f = domain (Lg (target f) X) by bw.
rewrite (csum_Cn h bf) /composef; aw; apply: f_equal;apply: Lg_exten.
by move => i isf /=; bw; rewrite -/(Vf f i); Wtac.
Qed.

Theorem cprod_Cn X f:
  target f = domain X -> bijection f ->
  card_prod X = card_prod (X \cf (graph f )).
Proof.
move=> tF bijf;apply /card_eqP.
exists (product_compose X f); hnf; rewrite lf_source lf_target.
split => //; first by apply: pc_fb.
rewrite /composef; aw; fct_tac.
Qed.

Theorem csum_An f g:
  partition_w_fam g (domain f) ->
  card_sum f = card_sumb (domain g) (fun l => card_sumb (Vg g l) (Vg f)).
Proof.
move=> pfg.
apply /card_eqP; set h := fun l:Set => _.
rewrite/disjointU/disjointU_fam Lg_domain.
set g0 := fun l:Set => _; set a:= unionb _.
have ->: a = unionb (Lg (domain g) (fun l => unionf (Vg g l) g0)).
  rewrite /a /unionb; bw; transitivity (unionf (domain f) g0).
    by apply: setUf_exten; move => t tdf /=; bw.
  rewrite - (proj33 pfg) /unionb setUf_A.
  apply: setUf_exten; move=> i idg /=; bw.
apply: equipotent_disjointU; fprops; bw; last first.
    apply: mutually_disjoint_prop2; move=> u v y _ _.
    by move /setX_P => [_ _ /set1_P <-] /setX_P [_ _ /set1_P].
  apply: mutually_disjoint_prop2; rewrite /g0=> u v y udg vdg; aw.
  move /setUf_P => [u' u'Vg /setX_P [py Py /set1_P Qy]].
  move /setUf_P => [v' v'Vg /setX_P [py' Py' /set1_P Qy']].
  case :(proj32 pfg _ _ udg vdg) =>// di.
  rewrite -Qy' Qy in v'Vg; case: (nondisjoint u'Vg v'Vg di).
split; fprops; bw => i idg; bw.
set g1:= (fun i0 => (Vg f i0 ) *s1 i0).
have ->: unionf (Vg g i) g1 = unionb (Lg (Vg g i) g1).
  rewrite /unionb; bw; apply: setUf_exten; move=> j jVg /=; bw.
eqtrans (h i).
rewrite /h /card_sumb /card_sum;eqtrans (disjointU (Lg (Vg g i) (Vg f))).
rewrite /disjointU/disjointU_fam; bw.
apply: equipotent_disjointU => //.
    split; fprops;bw; move=> j jVg; bw.
    apply: equipotent_setX; fprops.
  apply: mutually_disjoint_prop2; move=> u v y _ _; rewrite /g1.
  by move=> /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-].
apply: mutually_disjoint_prop2; move=> u v y _ _.
by move=> /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-].
Qed.

Theorem cprod_An f g:
  partition_w_fam g (domain f) ->
  card_prod f = card_prodb (domain g) (fun l => card_prodb (Vg g l) (Vg f)).
Proof.
move=> pfa; apply /card_eqP.
eqtrans(productb (Lg (domain g) (fun l => restriction_product f (Vg g l)))).
  exists (prod_assoc_map f g); split; first by apply: pam_fb.
  by rewrite/ prod_assoc_map; aw.
  by rewrite/ prod_assoc_map; aw.
apply: equipotent_setXb => //; split; fprops; bw.
move=> i idg; bw; rewrite /card_prodb /card_prod /restriction_product;fprops.
Qed.

Theorem cprod_sum_Dn f:
  card_prodb (domain f) (fun l => card_sum (Vg f l)) =
  card_sumb (productf (domain f) (fun l => (domain (Vg f l))))
    (fun g => (card_prod (Lg (domain f) (fun l => Vg (Vg f l) (Vg g l))))).
Proof.
apply /card_eqP.
eqtrans (productf (domain f) (fun l => (disjointU (Vg f l)))).
  apply: equipotent_setXb;split; fprops; bw.
  move=> i idf; bw; rewrite /card_sum; fprops.
set (g:= Lg (domain f) (fun l => disjointU_fam (Vg f l))).
have dg: domain g = domain f by rewrite /g; bw.
have ->: productf (domain f) (fun l => unionb (disjointU_fam (Vg f l))) =
    productf (domain g) (fun l => unionb (Vg g l)).
  rewrite -dg /productf;apply: f_equal; apply: Lg_exten.
  move=> x xdg; rewrite /g; bw; ue.
rewrite distrib_prod_union //.
set d0 := (productf (domain g) (fun l => domain (Vg g l))).
set g0:= fun g0:Set => _.
have ->: unionf d0 g0 = unionb (Lg d0 g0).
rewrite /unionb; bw;apply: setUf_exten; move=> i ip /=; bw.
rewrite /d0 dg.
set ld:= productf _ _.
have lde: ld = productf (domain f) (fun l => domain (Vg f l)).
  rewrite /ld/productf; apply: f_equal; apply: Lg_exten.
  move=> x xdg; rewrite /g; bw; rewrite / disjointU_fam; bw.
rewrite - lde.
apply: equipotent_disjointU;last by fprops.
  split => //; bw.
    rewrite/ disjointU_fam; bw.
    move=> i ip; bw.
    eqtrans (cardinal (productb (Lg (domain f)(fun l=> Vg (Vg f l) (Vg i l))))).
    eqtrans (productb (Lg (domain f) (fun l => Vg (Vg f l) (Vg i l)))).
    rewrite /productf; apply: equipotent_setXb; split => //; bw; fprops.
    move=> k kdg; rewrite /g /disjointU_fam -dg; bw.
      eqsym; fprops.
    move: ip; rewrite lde; move/setXf_P => [_ dif hyp].
    by apply: hyp; rewrite - dg.
  rewrite /disjointU_fam; bw; fprops.
have myel: forall i j y, inc i ld
    -> inc y (productf (domain f) (fun l => Vg (Vg g l) (Vg i l))) ->
  inc j (domain f) -> Q (Vg y j) = Vg i j.
  rewrite /g/ disjointU_fam.
  move=>k j y; bw=> kp1 yp jdf.
  move: kp1;rewrite lde;move /setXf_P=> [fgk dk kp1].
  move: (kp1 _ jdf)=> iVjk.
  move: yp => /setXf_P [fgy dy yp1].
  by move: (yp1 _ jdf); bw; move /setX_P => [_ _ /set1_P].
apply: mutually_disjoint_prop; bw.
move=>i j y ild jld; rewrite /g0 dg; bw=> xp yp.
apply: (setXf_exten ild jld) => k kdf /=.
by rewrite - (myel _ _ _ ild xp kdf) - (myel _ _ _ jld yp kdf).
Qed.

Product and sums of two cardinals

Definition card_sum2 a b := card_sum (variantLc a b).
Definition card_prod2 a b := card_prod (variantLc a b).

Notation "x +c y" := (card_sum2 x y) (at level 50).
Notation "x *c y" := (card_prod2 x y) (at level 40).

Lemma CS_sum2 a b: cardinalp (a +c b).
Proof. rewrite/card_sum2/card_sum; fprops. Qed.

Lemma CS_prod2 a b: cardinalp (a *c b).
Proof. rewrite /card_prod2/card_prod; fprops. Qed.

Hint Resolve CS_sum2 CS_prod2: fprops.

Lemma csum2_pr a b f: doubleton_fam f a b -> a +c b = card_sum f.
Proof.
move=> /two_terms_bij [g [bg tg ->]]; apply: (csum_Cn tg bg).
Qed.

Lemma cprod2_pr a b f: doubleton_fam f a b -> a *c b = card_prod f.
Proof. move=> /two_terms_bij [g [bg tg ->]]; apply: (cprod_Cn tg bg). Qed.

Lemma card_commutative_aux a b:
   doubleton_fam (variantLc b a) a b.
Proof. by exists C1, C0; bw;split; fprops; rewrite set2_C. Qed.

Lemma csumC a b: a +c b = b +c a.
Proof. apply: (csum2_pr (card_commutative_aux a b)). Qed.

Lemma cprodC a b: a *c b = b *c a.
Proof. by rewrite (cprod2_pr (card_commutative_aux a b)). Qed.

Lemma disjointU2_pr3 a b x y: y <> x ->
  (a +c b ) \Eq ((a *s1 x ) \cup (b *s1 y )).
Proof.
move=> yx.
rewrite -(disjointU2_rw _ _ yx) /card_sum2/card_sum.
have aux: forall z t, t <> z -> doubleton_fam (variantL z t a b) a b.
  move=> z t zt; exists z; exists t; split => //; bw.
  - by apply: nesym.
  - fprops.
  - rewrite /variantL; bw.
  - rewrite variant_V_a //.
  - rewrite variant_V_b //.
eqtrans (disjointU (variantL C0 C1 a b)).
by apply /card_eqP; move:(csum2_pr (aux _ _ yx)) (csum2_pr (aux _ _ TP_ne1)).
Qed.

Lemma disjointU2_pr4 a b:
  (a +c b ) \Eq ((a *s1 C0 ) \cup (b *s1 C1 )).
Proof. rewrite /card_sum2/card_sum -disjointU2_rw1; fprops. Qed.

Lemma csum2_pr5 a b: disjoint a b ->
  cardinal (a \cup b) = a +c b.
Proof.
move => h.
move: (CS_sum2 a b)=> cp; eq_aux.
apply/card_eqP; apply: equipotentT (equipotentS (disjointU2_pr4 a b)).
apply: (equipotent_disjointU2 h); fprops.
Qed.

Lemma csum2_pr4 a b a' b': a \Eq a' -> b \Eq b' ->
  a +c b = a' +c b'.
Proof.
move=> eaa' ebb.
rewrite - (card_card (CS_sum2 a b)) - (card_card (CS_sum2 a' b')).
apply /card_eqP.
move: (disjointU2_pr4 a b)(disjointU2_pr4 a' b')=> eq1 eq2.
apply: (equipotentT eq1); eqsym; apply: (equipotentT eq2).
apply: equipotent_disjointU2; fprops; rewrite /indexed; eqsym; fprops.
Qed.

Lemma csum2_pr2 a b a' b':
  cardinal a = cardinal a' -> cardinal b = cardinal b' ->
  a +c b = a' +c b'.
Proof. by move => /card_eqP p1 /card_eqP p2; apply: csum2_pr4. Qed.

Lemma csum2_pr2a x y: (cardinal x ) +c y = x +c y.
Proof. by apply: csum2_pr2; fprops; rewrite double_cardinal. Qed.

Lemma csum2_pr2b x y: x +c (cardinal y ) = x +c y.
Proof. by apply: csum2_pr2; fprops; rewrite double_cardinal. Qed.

Lemma cardinal_setC2 a b: sub a b ->
   cardinal b = a +c (b -s a ).
Proof.
by rewrite - (csum2_pr5 (set_I2Cr b a)) setU2_C; move /setCU_K => ->.
Qed.

Lemma cardinal_setC3 a b:
  (a -s b ) \Eq (b -s a ) -> a \Eq b.
Proof.
move /card_eqP => h; apply /card_eqP.
rewrite (cardinal_setC2 (@subsetI2l a b)) (cardinal_setC2 (@subsetI2r a b)).
move: (set_CI2 a b a); rewrite setC_v set0_U2 => ->.
rewrite - csum2_pr2b h csum2_pr2b.
by move: (set_CI2 b a b); rewrite setC_v set0_U2 setI2_C => ->.
Qed.

Lemma cprod2_pr1 a b:
  a *c b = cardinal (a \times b).
Proof.
have h:= (product2_canon_fb a b).
apply/card_eqP; eqsym.
exists (product2_canon a b); split => //;rewrite/product2_canon; aw.
Qed.

Lemma cprod2_pr2 a b a' b':
  cardinal a = cardinal a' -> cardinal b = cardinal b' ->
  a *c b = a' *c b'.
Proof.
move=> /card_eqP caa' /card_eqP cbb'.
by rewrite ! cprod2_pr1; apply/card_eqP /equipotent_setX.
Qed.

Lemma cprod2_pr2b x y: x *c (cardinal y ) = x *c y.
Proof. by apply: cprod2_pr2; fprops; rewrite double_cardinal. Qed.

Lemma cprod2_pr2a x y: (cardinal x ) *c y = x *c y.
Proof. by apply: cprod2_pr2; fprops; rewrite double_cardinal. Qed.

Definition quasi_bij X f I :=
  [/\ (forall x, inc x I -> inc (f x) (domain X)),
  (forall x y, inc x I -> inc y I -> f x = f y -> x = y) &
  (forall y, inc y (domain X)-> exists2 x, inc x I & y = f x)].

Lemma cardinal_commutativity_aux X f I (F := (Lf f I (domain X))) :
  quasi_bij X f I ->
  [/\ target F = domain X, bijection F &
    X \cf (graph F ) = Lg I (fun z => Vg X (f z))].
Proof.
move=> [p1 p2 p3].
rewrite /F; aw;split => //; first by apply: lf_bijective.
rewrite /composef;aw; last by apply:lf_function.
apply: fgraph_exten;bw; fprops.
move => t tI /=; bw; rewrite -/(Vf _ _); aw.
Qed.

Lemma csum_Cn2 X f I: quasi_bij X f I ->
  card_sum X = card_sumb I (fun z => Vg X (f z)).
Proof.
move=> h; move:(cardinal_commutativity_aux h) => [tF bF vF].
by rewrite (csum_Cn tF bF) vF.
Qed.

Lemma cprod_Cn2 X f I: quasi_bij X f I ->
  card_prod X = card_prodb I (fun z => Vg X (f z)).
Proof.
move=> h; move:(cardinal_commutativity_aux h) => [tF bF vF].
by rewrite (cprod_Cn tF bF) vF.
Qed.

Lemma sum_of_sums_aux I f g:
  (card_sumb I f ) +c (card_sumb I g ) = card_sumb I (fun i => (f i ) +c (g i )) /\
  (card_prodb I f ) *c (card_prodb I g ) = card_prodb I (fun i => (f i ) *c (g i )).
Proof.
set K := I \times C2.
set K1 := I *s1 C0.
set K2 := I *s1 C1.
pose R i := indexedr i C2.
set h := Lg I R.
set k := fun p=> Yo (Q p = C0) (f (P p)) (g (P p)).
set G:= variantLc K1 K2.
have uK: K = K1 \cup K2 by rewrite /K/K1/K2 - distrib_union_prod2 setU2_11.
have sk1: sub K1 K by move=> t; rewrite uK; fprops.
have sk2: sub K2 K by move=> t; rewrite uK; fprops.
have ue: K1 \cap K2 = emptyset.
  rewrite /K1 /K2 - distrib_inter_prod2.
  apply /set0_P => t /setX_P [_ _ /setI2_P [] /set1_P -> /set1_P]; fprops.
have pfa: partition_w_fam G (domain (Lg K k)).
  by red;rewrite /G;split; fprops; [apply: disjointLv| bw; rewrite - union2Lv ].
have kp1: forall p, k (J p C0) = f p by move=> p; rewrite /k; aw; Ytac0.
have kp2: forall p, k (J p C1) = g p by move=> p; rewrite /k; aw;Ytac0.
have p1: forall x, inc x I -> sub (R x) K.
   move=> x xI t /setX_P [pt /set1_P pa pb]; apply: setX_i => //; ue.
have pf1: partition_w_fam h (domain (Lg K k)).
  red; rewrite /h; split; fprops.
    apply: mutually_disjoint_prop2; move=> i j y _ _.
    by move /setX_P => [_ /set1_P <- _] /setX_P [_ /set1_P <- _].
  bw; set_extens t.
    by move/setUf_P; bw; move => [y yI];bw; apply: p1.
  move => /setX_P [tp Pi Qt]; apply /setUb_P; bw; ex_tac; bw.
  apply /setX_i; fprops.
set X1 := (Lg K1 (Vg (Lg K k))).
set X2 := (Lg K2 (Vg (Lg K k))).
have pa: (quasi_bij X1 (fun p=> J p C0) I).
  rewrite /X1 /quasi_bij; bw;split => //.
  - move=> x xI; apply /setXp_i; fprops.
  - by move=> x y _ _ q; apply: (pr1_def q).
  - rewrite /X1/K1; bw; move=> y /setX_P [py pI /set1_P <-]; ex_tac; aw.
have pa': (quasi_bij X2 (fun p=> J p C1) I).
  rewrite /X2 /quasi_bij; bw;split => //.
  - move=> x xI; apply /setXp_i; fprops.
  - by move=> x y _ _ q; apply: (pr1_def q).
  - rewrite /X2/K2; bw; move=> y /setX_P [py pI /set1_P <-]; ex_tac; aw.
have sf1: Lg I (fun z => Vg X1 (J z C0)) = Lg I f.
   apply: Lg_exten => x xI.
   have p3: inc (J x C0) K1 by apply: setXp_i; fprops.
   by rewrite /X1;bw; apply: sk1.
have sf2: Lg I (fun z => Vg X2 (J z C1)) = Lg I g.
   apply: Lg_exten => x xI.
   have p3: inc (J x C1) K2 by apply: setXp_i; fprops.
   by rewrite /X2;bw; apply: sk2.
move: (csum_Cn2 pa)(cprod_Cn2 pa)(csum_Cn2 pa')(cprod_Cn2 pa').
rewrite /card_sumb /card_prodb - sf1 - sf2;move => <- <- <- <-.
clear pa pa' sf1 sf2.
move: (csum_An pfa) (cprod_An pfa); rewrite /card_sumb /card_prodb.
set f1 := Lg (domain _) _; set f2 := Lg (domain _) _.
have ->: f1 = variantLc (card_sum X1) (card_sum X2).
  rewrite /f1 /variantLc /variantL /G; bw.
  symmetry;apply: Lg_exten => x /C2_P; case; move=> ->;bw.
have ->: f2 = variantLc (card_prod X1) (card_prod X2).
  rewrite /f2 /variantLc /variantL /G; bw.
  symmetry;apply: Lg_exten => x /C2_P; case; move=> ->;bw.
rewrite {1} /card_sum2; move => <-.
rewrite {1} /card_prod2; move => <-.
clear pfa G f1 f2 X1 X2.
have dh: domain h = I by rewrite /h; bw.
rewrite (csum_An pf1) (cprod_An pf1) dh /card_sumb /card_prodb.
have dfI: forall x, inc x I ->
   doubleton_fam (Lg (R x) (Vg (Lg K k))) (f x) (g x).
  move => x xI.
  have p2: sub (R x) (domain (Lg K k)) by bw; apply: p1.
  have fK:inc (J x C0) K by apply: sk1; apply: setXp_i; fprops.
  have sK:inc (J x C1) K by apply: sk2; apply: setXp_i; fprops.
  have pa: inc (J x C0) (R x) by apply: setXp_i; fprops.
  have pb: inc (J x C1) (R x) by apply: setXp_i; fprops.
  exists (J x C0); exists (J x C1).
  have fgk: fgraph (Lg K k) by fprops.
  have xa: J x C0 <> J x C1 by move => H; move: (pr2_def H); apply: TP_ne.
  have xb: domain (Lg (R x) (Vg (Lg K k))) = doubleton (J x C0) (J x C1).
    bw; set_extens t; last by by case /set2_P => ->.
    move /setX_P => [qa /set1_P qb /C2_P].
    case =>qc; rewrite -qa qb qc; fprops.
  split => //; fprops; bw; try apply: (p1 _ xI); rewrite kp1 kp2.
split;apply: f_equal; apply: Lg_exten;move => x xI; rewrite /h; bw.
  by symmetry; apply: csum2_pr; apply: dfI.
by symmetry; apply: cprod2_pr; apply: dfI.
Qed.

Lemma sum_of_sums f g I:
(card_sumb I f ) +c (card_sumb I g ) = card_sumb I (fun i => (f i ) +c (g i )).
Proof. exact (proj1 (sum_of_sums_aux I f g)). Qed.

Lemma prod_of_prods f g I:
  (card_prodb I f ) *c (card_prodb I g ) = card_prodb I (fun i =>(f i ) *c (g i )).
Proof. exact (proj2 (sum_of_sums_aux I f g)). Qed.

Lemma cprodA a b c: a *c (b *c c ) = (a *c b ) *c c.
Proof.
rewrite ! cprod2_pr1; apply/card_eqP.
eqtrans (product a (product b c)).
eqtrans (product (product a b) c).
apply: product2A.
Qed.

Lemma csumA a b c: a +c (b +c c ) = (a +c b ) +c c.
Proof.
move: a b c.
have aux: (forall u v w a b c, v <> u-> u <> w -> w <> v ->
  a +c (b +c c ) =
  cardinal ((a *s1 u ) \cup ((b *s1 v ) \cup (c *s1 w )))).
  move=> u v w a b c vu uw wv.
  move: (disjointU2_pr3 a (b +c c) vu) => p1.
  move: (disjointU2_pr3 b c wv)=> p2.
  have cabc: cardinalp (a +c (b +c c)) by fprops.
  eq_aux; apply/card_eqP.
  apply (equipotentT p1).
  apply: equipotent_disjointU2; fprops.
    apply: disjoint_pr; move=> z; move /setX_P => [_ _ /set1_P pa]
    /setU2_P [] /setX_P [_ _ /set1_P]; rewrite pa => //; apply:nesym => //.
  eqtrans (b +c c); eqsym; fprops.
move: card1_nz => ne1.
have ne2: \2 c <> \1 c by move: card_12; apply:nesym.
have ne3: \0 c <> \2 c by move: card2_nz; apply:nesym.
move=> a b c.
rewrite - (csumC c (a +c b)).
rewrite(aux _ _ _ a b c ne1 ne3 ne2) (aux _ _ _ c a b ne3 ne2 ne1).
by rewrite setU2_A setU2_C.
Qed.

Lemma csum_permute24: interchange card_sum2 card_sum2.
Proof.
move => s1 s2 r1 r2; rewrite (csumA _ s2 r2) (csumA _ r1 r2).
by rewrite -(csumA s1) (csumC s2 r1) (csumA s1).
Qed.

Lemma cprod_sumDl a b c:
  a *c (b +c c ) = (a *c b ) +c (a *c c ).
Proof.
have aux: forall a b c, (a \times (b *s1 c )) \Eq ((a *c b ) *s1 c ).
  move=> a' b' c'; eqtrans ((a' \times b') *s1 c').
    apply: product2A.
  apply: equipotent_setX; fprops;rewrite cprod2_pr1; fprops.
rewrite cprod2_pr1.
have cabab: cardinalp ((a *c b) +c (a *c c)) by fprops.
eq_aux;apply/card_eqP.
eqtrans (product a ((b *s1 C0 ) \cup (c *s1 C1 ))).
  apply: equipotent_setX; fprops; apply: disjointU2_pr4.
rewrite distrib_union_prod2 //.
eqtrans (disjointU (variantLc (a *c b) (a *c c))); last first.
  eqsym; rewrite disjointU2_rw1; apply: disjointU2_pr4.
rewrite disjointU2_rw1; apply: equipotent_disjointU2.
- by apply: disjointU2_pr0; apply: disjointU2_pr; fprops.
- by apply: disjointU2_pr; fprops.
- by apply: aux.
- by apply: aux.
Qed.

Lemma cprod_sumDr a b c:
  (b +c c ) *c a = (b *c a ) +c (c *c a ).
Proof.
rewrite cprodC (cprodC b a) (cprodC c a); apply: cprod_sumDl.
Qed.

Lemma cprod2_sumDn a f:
  a *c (card_sum f ) = card_sumb (domain f) (fun i => a *c (Vg f i )).
Proof.
rewrite cprod2_pr1 /card_sum; apply /card_eqP.
eqtrans (product a (disjointU f)).
rewrite/disjointU distrib_prod2_sum /disjointU_fam; bw.
apply: equipotent_disjointU => //.
- split => //; fprops; bw;move=> i idf; bw.
  eqtrans (product (product a (Vg f i)) (singleton i)).
    apply: product2A.
  apply: equipotent_setX; fprops;rewrite cprod2_pr1; fprops.
- apply: mutually_disjoint_prop2=> i j y idf jdf; bw.
  move => /setX_P [_ _ /setX_P [_ _ /set1_P <-]].
  by move => /setX_P [_ _ /setX_P [_ _ /set1_P <-]].
- apply: mutually_disjoint_prop2=> i j y idf jdf; bw.
  by move => /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-].
Qed.

EIII-3-4 Properties of the cardinals 0 and 1

Lemma csum_trivial f: domain f = emptyset ->
  card_sum f = \0 c.
Proof.
move=> dge; rewrite/card_sum /disjointU /disjointU_fam dge /Lg funI_set0.
by rewrite setUb_0 cardinal_set0.
Qed.

Lemma cprod_trivial f: domain f = emptyset ->
  card_prod f = \1 c.
Proof.
by move=> /domain_set0_P ->; rewrite/card_prod setXb_0 cardinal_set1.
Qed.

Lemma csum_trivial2 x f: domain f = singleton x ->
  card_sum f = cardinal (Vg f x).
Proof.
move=> df; rewrite/card_sum /disjointU/disjointU_fam; aw.
rewrite df /unionb Lg_domain setUf_1; bw;[ apply /card_eqP; eqsym |];fprops.
Qed.

Lemma cprod_trivial2 x f: domain f = singleton x ->
  card_prod f = cardinal (Vg f x).
Proof.
move=> df; apply /card_eqP.
eqsym; exists (product1_canon (Vg f x) x); split.
  apply: setX1_canon_fb.
rewrite /product1_canon; aw.
by rewrite/ product1_canon; aw;apply: setX1_pr2.
Qed.

Lemma csum_trivial1 x f: domain f = singleton x ->
  cardinalp (Vg f x) -> card_sum f = Vg f x.
Proof.
move=> df cV; by rewrite (csum_trivial2 df) (card_card cV).
Qed.

Lemma cprod_trivial1 x f: domain f = singleton x ->
  cardinalp (Vg f x) -> card_prod f = Vg f x.
Proof.
by move=> df cV; rewrite (cprod_trivial2 df) (card_card cV).
Qed.

Lemma csum_trivial3 x a: cardinalp a ->
  card_sum (cst_graph (singleton x) a) = a.
Proof.
move=> xa; rewrite/ cst_graph (csum_trivial1 (x:=x)); bw; fprops.
Qed.

Lemma csumA_setU2 A B f: disjoint A B ->
  card_sumb (A \cup B) f = card_sumb A f +c card_sumb B f.
Proof.
move => dab; rewrite /card_sumb.
pose h := Lg (A \cup B) f.
set g := variantLc A B.
have pa: partition_w_fam g (domain h).
  rewrite /h /g; bw; red; rewrite union2Lv;split; fprops.
  move => i j; bw; case/C2_P => ->; case/C2_P => ->; bw; fprops.
  by right; apply: disjoint_S.
rewrite (csum_An pa) /card_sumb; symmetry; apply: csum2_pr.
have pb: inc C1 C2 by fprops.
have pc: inc C0 C2 by fprops.
rewrite /g;bw;exists C0, C1; bw; rewrite /h.
split;fprops; apply: csumb_exten => t ts;bw; fprops.
Qed.

Lemma csumA_setU1 A b f: ~ (inc b A ) ->
  card_sumb (A +s1 b) f = card_sumb A f +c (f b ).
Proof.
move => pa.
transitivity (card_sumb A f +c cardinal (f b)); last by apply:csum2_pr4; fprops.
have pc: disjoint A (singleton b).
  by apply: disjoint_pr => t tA /set1_P tb; case:pa; rewrite - tb.
set g := (Lg (singleton b) f).
have dg: domain g = singleton b by rewrite /g; bw.
have <-: Vg g b = f b by rewrite /g; bw; fprops.
by rewrite (csumA_setU2 _ pc) - (csum_trivial2 dg).
Qed.

Lemma cprodA_setU2 A B f: disjoint A B ->
  card_prodb (A \cup B) f = card_prodb A f *c card_prodb B f.
Proof.
move => dab; rewrite /card_prodb.
pose h := Lg (A \cup B) f.
set g := variantLc A B.
have pa: partition_w_fam g (domain h).
  rewrite /h /g; bw; red; rewrite union2Lv;split; fprops.
  move => i j; bw; case/C2_P => ->; case/C2_P => ->; bw; fprops.
  by right; apply: disjoint_S.
rewrite (cprod_An pa) /card_prodb; symmetry; apply: cprod2_pr.
have pb: inc C1 C2 by fprops.
have pc: inc C0 C2 by fprops.
rewrite /g;bw;exists C0, C1; bw; rewrite /h.
split;fprops; apply: cprodb_exten => t ts;bw; fprops.
Qed.

Lemma cprodA_setU1 A b f: ~ (inc b A ) ->
  card_prodb (A +s1 b) f = card_prodb A f *c (f b ).
Proof.
move => pa.
transitivity (card_prodb A f *c cardinal (f b)); last first.
  by apply: cprod2_pr2; fprops; rewrite double_cardinal.
have pc: disjoint A (singleton b).
  by apply: disjoint_pr => t tA /set1_P tb; case: pa; rewrite - tb.
set g := (Lg (singleton b) f).
have dg: domain g = singleton b by rewrite /g; bw.
have <-: Vg g b = f b by rewrite /g; bw; fprops.
by rewrite (cprodA_setU2 _ pc) - (cprod_trivial2 dg).
Qed.

Lemma card_partition_induced X f F:
  (forall x, inc x X -> inc (f x) F) ->
  cardinal X = card_sumb F (fun k => cardinal (Zo X (fun z => f z = k))).
Proof.
move => fim.
pose g k := Zo X (fun z => f z = k).
move: (@disjointU_disjoint (Lg F g)) => pa.
move: (csum_pr (Lg F g)).
have <- : card_sumb (domain (Lg F g)) (fun a => cardinal (Vg (Lg F g) a))
  = card_sumb F(fun k => cardinal (Zo X (fun z => f z = k))).
   bw; apply: csumb_exten => i ie; rewrite /g; bw.
move => <-;apply /card_eqP.
rewrite /disjointU /disjointU_fam /g; bw.
set S := unionb _.
pose h x := J x (f x).
exists (Lf h X S); red; aw;split => //; apply lf_bijective.
    move => x xX; move: (fim _ xX) => ok.
    by apply /setUb_P; bw; ex_tac; bw; apply: indexed_pi; apply /Zo_P.
  move => u v _ _ sv; exact: (pr1_def sv).
move => y /setUb_P; bw; move => [z zf]; bw.
move =>/indexed_P [px /Zo_P [pc pd] pe];ex_tac.
by rewrite -{1} px /h pd pe.
Qed.

Lemma card_partition_induced1 X f F g:
  (forall x, inc x X -> inc (f x) F) ->
  card_sumb X g = card_sumb F (fun i => card_sumb (Zo X (fun z => f z = i)) g).
Proof.
move => fim.
pose h i := (Zo X (fun z => f z = i)).
have pa: (partition_w_fam (Lg F h) (domain (Lg X g))).
  bw; split; first by fprops.
    rewrite /h; red; bw => i j iF jF; bw; mdi_tac eq1 => u /Zo_hi fu.
    by move /Zo_hi => fv; case: eq1; rewrite -fu fv.
  rewrite /h;set_extens t.
    by move /setUb_P; bw; move => [y yf]; bw; move => /Zo_P [].
  move => tx; apply /setUb_P; bw; move: (fim _ tx) => ft; ex_tac; bw.
  by apply /Zo_P.
rewrite {1} /card_sumb (csum_An pa); bw.
apply: csumb_exten => i iF; rewrite /h; bw.
apply:csumb_exten => z zi; bw; apply: Zo_S zi.
Qed.

Theorem csum_zero_unit f j:
  sub j (domain f) ->
  (forall i, inc i ((domain f ) -s j) -> (Vg f i ) = \0 c) ->
  card_sum f = card_sumb j (Vg f).
Proof.
move=> jdf acz; congr (cardinal _).
rewrite /disjointU/disjointU_fam; bw.
set_extens x; move /setUb_P; bw; move => [y yd]; bw => h; apply/setUb_P; bw.
  case: (inc_or_not y j)=> yj; first by ex_tac; bw.
  have yc: (inc y ((domain f) -s j)) by apply /setC_P.
  move: h; rewrite (acz _ yc)=> /setX_P [_ pe _].
  case: (in_set0 pe).
by exists y; bw; apply: jdf.
Qed.

Theorem cprod_one_unit f j:
  sub j (domain f) ->
  (forall i, inc i ((domain f ) -s j) -> (Vg f i ) = \1 c) ->
  card_prod f = card_prodb j (Vg f).
Proof.
move=> jdf alo; apply /card_eqP; exists (pr_j f j); split.
- by apply: prj_fb=>// i ici; rewrite (alo _ ici); exists emptyset.
- by rewrite /pr_j; aw.
- by rewrite /pr_j; aw.
Qed.

Lemma csum0r a: cardinalp a -> a +c \0 c = a.
Proof.
move=> ca.
rewrite -{2} (card_card ca) - (card_card (CS_sum2 a \0 c)).
apply/card_eqP; eqtrans (a *s1 C0); last by eqsym; fprops.
by move: (disjointU2_pr4 a \0 c); rewrite /indexed setX_0l setU2_0.
Qed.

Lemma cprod1r a: cardinalp a -> a *c \1 c = a.
Proof.
move=> ca; rewrite cprod2_pr1; eq_aux;apply /card_eqP.
eqtrans (cardinal a);eqsym; apply: equipotent_indexed.
Qed.

Hint Rewrite csum0r cprod1r: aw.

Lemma csum0l a: cardinalp a -> \0 c +c a = a.
Proof. move=> ca; rewrite csumC; aw. Qed.

Lemma cprod1l a: cardinalp a -> \1 c *c a = a.
Proof. move=> ca; rewrite cprodC; aw. Qed.

Hint Rewrite csum0l cprod1l: aw.

Lemma cprod0r a: a *c \0 c = \0 c.
Proof. rewrite cprod2_pr1 /card_zero; aw; bw; apply: cardinal_set0. Qed.

Lemma cprod_zero_absorbing f:
  (exists2 i, inc i (domain f) & cardinal (Vg f i) = \0 c)
  -> card_prod f = \0 c.
Proof.
move=> [i idf cVz];rewrite /card_prod.
case: (emptyset_dichot (productb f)); first by move => ->; apply: cardinal_set0.
by move /setXb_ne2 => h; move: (h i idf)=> /cardinal_nonemptyset1.
Qed.

Lemma csum_of_ones b: card_sum (cst_graph b \1 c) = cardinal b.
Proof.
rewrite/card_sum /disjointU/disjointU_fam; bw.
set f:= Lg _ _.
have fv: (f= Lg b (fun i=> \1 c *s1 i)).
   rewrite /f/cst_graph; apply: Lg_exten => x xj /=; bw.
have ->: (unionb f = \1 c \times b).
  rewrite fv;set_extens t.
    move=> /setUb_P; bw ; move => [y yj]; bw.
    move => /setX_P [pa pb /set1_P pc]; apply /setX_P;split => //; ue.
  move /setX_P => [pa pb pc]; apply/setUb_P; bw; ex_tac; bw.
  apply:setX_i;fprops.
apply/card_eqP;eqsym;apply: equipotent_rindexed.
Qed.

Lemma csum_of_ones1 b j: cardinalp b -> b \Eq j ->
  card_sum (cst_graph j \1 c) = b.
Proof.
move=> cb bj; rewrite csum_of_ones - (card_card cb).
by symmetry; apply/card_eqP.
Qed.

Lemma csum_of_same a b: card_sum (cst_graph b a) = a *c b.
Proof.
move: (csum_of_ones b)=> p.
have cca: cardinalp (cardinal a) by fprops.
have -> : a *c b = cardinal a *c cardinal b.
  by apply: cprod2_pr2; rewrite double_cardinal.
rewrite - p cprod2_sumDn; bw.
apply: csum_pr3; bw; fprops.
by move=> i ib; bw; rewrite cprod1r; fprops; rewrite double_cardinal.
Qed.

Lemma csum_of_same1 a b j:
  cardinalp a -> cardinalp b -> b \Eq j ->
  card_sum (cst_graph j a) = a *c b.
Proof.
move=> ca cb bj; symmetry.
by rewrite csum_of_same; apply: cprod2_pr2 => //; apply/card_eqP.
Qed.

Lemma card_succ_pr3 x: succ (cardinal x) = x +c \1 c.
Proof.
have p: disjoint (cardinal x) (singleton (cardinal x)).
  apply /set0_P => y /setI2_P [pa] /set1_P => pb.
  by case: (cardinal_irreflexive (CS_cardinal x)); rewrite -{1} pb.
by rewrite /succ (csum2_pr5 p) - csum2_pr2b csum2_pr2a cardinal_set1.
Qed.

Lemma card_succ_pr4 x: cardinalp x -> succ x = x +c \1 c.
Proof. by rewrite - card_succ_pr3;move /card_card => ->. Qed.

Lemma card_succ_pr5 a: cardinal (succ a) = succ a.
Proof. apply: (card_card (CS_succ a)). Qed.

Lemma card_two_pr: \1 c +c \1 c = \2 c.
Proof. by rewrite - (card_succ_pr4 CS1) succ_one. Qed.

Lemma two_times_n n: \2 c *c n = n +c n.
Proof.
set (m:= cardinal n).
have cm: cardinalp m by rewrite /m;fprops.
have ->: n +c n = m +c m by apply: csum2_pr2; rewrite double_cardinal.
have <- : \2 c *c m = \2 c *c n by apply cprod2_pr2b.
rewrite - card_two_pr cprod_sumDr; aw.
Qed.

Definition card_nz_fam f := (forall i, inc i (domain f) -> Vg f i <> \0 c).

Theorem cprod_nzP f: card_nz_fam f <-> (card_prod f <> \0 c ).
Proof.
split => h.
  rewrite/card_prod /card_zero.
  have alne: (forall i, inc i (domain f) -> nonempty (Vg f i)).
    move=> i idf; move: (h _ idf)=> vz.
    case: (emptyset_dichot (Vg f i))=> // p.
  move: (setXb_ne alne); apply: cardinal_nonemptyset1.
move=> i idf; dneg vz; apply: cprod_zero_absorbing=>//; ex_tac.
by rewrite vz; apply: cardinal_set0.
Qed.

Lemma cprod2_nz a b: a <> \0 c -> b <> \0 c -> a *c b <> \0 c.
Proof.
move=> az bz; apply /cprod_nzP; red; bw => i itp;try_lvariant itp.
Qed.

Theorem succ_injective a b: cardinalp a -> cardinalp b ->
  a +c \1 c = b +c \1 c -> a = b.
Proof.
move=> ca cb.
rewrite - (card_succ_pr4 ca)- (card_succ_pr4 cb).
by apply: succ_injective1.
Qed.

EIII-3-5 Exponentiation of cardinals

Definition card_pow a b := cardinal (functions b a).
Notation "x ^c y" := (card_pow x y) (at level 30).

Lemma CS_pow: forall a b, cardinalp (a ^c b).
Proof. rewrite /card_pow; fprops. Qed.

Hint Resolve CS_pow: fprops.

Lemma cpow_pr a b a' b':
  a \Eq a' -> b \Eq b' -> a ^c b = a' ^c b'.
Proof.
move=> [f [bf sf tf]] ebb'; apply /card_eqP.
move: (equipotentS ebb')=> [g [bg sg tg]].
exists (compose3function g f); red.
rewrite {2 3} /compose3function - sf -tf - sg -tg; aw.
by split => //;apply: c3f_fb.
Qed.

Lemma cpow_pra a b: (cardinal a ) ^c b = a ^c b.
Proof. apply: cpow_pr; fprops. Qed.

Lemma cpow_prb a b: a ^c (cardinal b ) = a ^c b.
Proof. apply: cpow_pr; fprops. Qed.

Theorem cpow_pr1 x y:
  cardinal (functions y x) = (cardinal x ) ^c (cardinal y ).
Proof. apply: cpow_pr; fprops. Qed.

Lemma cpow_pr2 a b:
  card_prod (cst_graph b a) = a ^c b.
Proof.
apply/card_eqP.
rewrite (setXb_eq_graphset (f:= (cst_graph b a)) (x:=a)) //;bw.
  eqsym; apply: fun_set_equipotent.
move=> i isc;bw.
Qed.

Theorem cpow_pr3 a b j: cardinal j = b ->
  card_prod (cst_graph j a) = a ^c b.
Proof.
move=> cj;transitivity (a ^c j); first by apply: cpow_pr2.
rewrite -cj; apply: cpow_pr; fprops.
Qed.

Lemma cpow_sum a f:
  a ^c (card_sum f ) =
  card_prodb (domain f) (fun i => a ^c (Vg f i )).
Proof.
transitivity (a ^c (disjointU (Lg (domain f) (Vg f)))).
  apply: cpow_pr; fprops.
rewrite - (card_sum_gr) /card_sum; eqsym; fprops.
rewrite -cpow_pr2 /disjointU.
set S:= disjointU_fam _; set f0:= cst_graph _ _.
have pfa:partition_w_fam S (domain f0).
  move: (partition_disjointU (Lg (domain f) (Vg f))); rewrite /f0; bw.
rewrite (cprod_An pfa).
rewrite /S /disjointU_fam ! Lg_domain;apply cprodb_exten.
move=> x xdf /=; bw; rewrite /card_prodb.
have ->: (Lg (Vg f x *s1 x) (Vg f0)) = (Lg (Vg f x *s1 x) (fun _ => a)).
  rewrite /f0;apply: Lg_exten => t tw; bw.
  apply /setUb_P; rewrite /S /disjointU_fam;bw; ex_tac; bw.
rewrite cpow_pr2; apply: cpow_pr; fprops; eqsym; fprops.
Qed.

Lemma cpow_prod b f:
  (card_prod f ) ^c b = card_prodb (domain f) (fun i => (Vg f i ) ^c b).
Proof.
rewrite - cpow_pr2.
set (g:= Lg (product (domain f) b)(fun z=> Vg f (P z))).
set (h0:= Lg (domain f) (fun i => product (singleton i) b)).
have fph0: partition_w_fam h0 (domain g).
  red; rewrite /h0; split; fprops.
    apply: mutually_disjoint_prop2; move=> i j y _ _.
    by move => /setX_P [_ /set1_P <- _] /setX_P [_ /set1_P <- _].
  set_extens t.
    move => /setUb_P; bw; move => [y yd]; rewrite /g; bw.
    move /setX_P => [pa /set1_P pb pc]; apply:setX_i => //; ue.
  rewrite /g; bw => /setX_P [pa pb pc]; apply /setUb_P; bw; ex_tac.
  bw; apply /setX_P; split;fprops.
rewrite /card_prodb.
have <-: (Lg (domain f) (fun l => card_prodb (Vg h0 l) (Vg g))=
    Lg (domain f) (fun i => (Vg f i ) ^c b)).
  apply: Lg_exten.
  move=> x xsf; rewrite /h0; bw; rewrite /card_prodb.
  set (T:= indexedr x b).
  have ->: ( (Lg (singleton x \times b) (Vg g)) = cst_graph T (Vg f x)).
      rewrite /g; apply: fgraph_exten; fprops; bw => t ts.
      move /setX_P: (ts) => [pa /set1_P pb pc]; bw; first by ue.
      by apply /setX_P;split => //; rewrite pb.
  rewrite cpow_pr2; apply: cpow_pr; fprops.
  rewrite /T; eqsym; apply: equipotent_rindexed.
have dh0: domain h0 = domain f by rewrite /h0; bw.
move: (cprod_An fph0).
rewrite dh0 /card_prodb => <-; clear dh0.
set (h:= Lg b (fun i => (domain f) *s1 i)).
have pfa: (partition_w_fam h (domain g)).
  rewrite/ h;split; fprops.
  apply: mutually_disjoint_prop2; move=> i j y _ _.
    by move=> /setX_P [_ _ /set1_P <-] /setX_P [_ _ /set1_P <-].
  set_extens t; rewrite /g; bw.
    move => /setUb_P; bw; move => [y yd]; bw; move /setX_P => [pa pb].
    move /set1_P => pc; apply: setX_i;fprops; ue.
  move => /setX_P [pa pb pc]; apply /setUb_P; bw; ex_tac; bw.
  apply:setX_i; fprops.
rewrite (cprod_An pfa).
have ->: (domain h = b) by rewrite /h; bw.
symmetry; apply: cprodb_exten =>// x xb; rewrite /card_prodb.
have ->: (Lg (Vg h x) (Vg g)) = Lg ((domain f) *s1 x) (fun z => Vg f(P z)).
  rewrite /h; bw; apply: Lg_exten => t ts; rewrite /g; bw.
  move /setX_P: ts => [pa pb /set1_P pc]; apply /setX_P;split => //; ue.
set (ff:=Lf (fun u=> J u x) (domain f) ( (domain f) *s1 x)).
set (X :=Lg (product (domain f) (singleton x)) (fun z => Vg f (P z))).
have fgX: fgraph X by rewrite /X; fprops.
have tff: target ff = domain X by rewrite / ff/X; aw; bw.
have bff: (bijection ff).
   rewrite /ff/indexed; apply: lf_bijective.
   - by move=> t xa /=; aw; fprops.
   - by move=> u v _ _; apply: pr1_def.
   - by move=> y /setX_P [py Pya /set1_P <-]; ex_tac; aw.
rewrite (cprod_Cn tff bff) -(card_prod_gr f).
have -> //: (X \cf (graph ff) = Lg (domain f) (Vg f)).
move:(bij_function bff) => fff.
rewrite /composef /ff; aw; bw.
apply: fgraph_exten; fprops; bw.
have lfa: lf_axiom (J^~ x) (domain f) (domain f *s1 x).
   by move=> z; aw=> zf; apply: setXp_i; fprops.
move => t tf /=; bw; rewrite -/(Vf ff t) (lf_V lfa tf) /X; bw;aw; fprops.
Qed.

Lemma cpow_sum2 a b c: a ^c (b +c c ) = (a ^c b ) *c (a ^c c ).
Proof.
rewrite /card_sum2 cpow_sum; symmetry; apply: cprod2_pr; bw.
move: (doubleton_fam_canon (fun i => card_pow a (Vg (variantLc b c) i))).
bw.
Qed.

Lemma cpow_prod2 a b c: (a *c b ) ^c c = (a ^c c ) *c (b ^c c ).
Proof.
rewrite {2} /card_prod2 cpow_prod; bw; symmetry; apply: cprod2_pr.
move: (doubleton_fam_canon (fun i => card_pow (Vg (variantLc a b) i) c)).
bw.
Qed.

Lemma cpow_pow a b c: a ^c (b *c c ) = (a ^c b ) ^c c.
Proof.
rewrite -csum_of_same cpow_sum.
rewrite -cpow_pr2; bw; congr (card_prod _); apply: Lg_exten=>// => x xc ; bw.
Qed.

Lemma cpowx0 a: a ^c \0 c = \1 c.
Proof.
rewrite - (csum_trivial domain_set0) cpow_sum.
apply: cprod_trivial; fprops; bw.
Qed.

Lemma cpow00: \0 c ^c \0 c = \1 c.
Proof. apply: cpowx0. Qed.

Lemma cpowx1c a: a ^c \1 c = cardinal a.
Proof.
set (b := cardinal a).
transitivity (b ^c \1 c).
  rewrite/b;apply: cpow_pr; fprops.
rewrite - cpow_pr2 /cst_graph; set f := Lg _ _.
have df: (domain f = singleton emptyset) by rewrite /f; bw.
have Vf: (Vg f emptyset = b) by rewrite /f/card_one; bw; fprops.
have cVa: (cardinalp (Vg f emptyset)) by rewrite Vf /b; fprops.
rewrite -Vf; apply: (cprod_trivial1 df cVa).
Qed.

Lemma cpowx1 a: cardinalp a -> a ^c \1 c = a.
Proof. by move=> ac; rewrite cpowx1c; apply: card_card. Qed.

Lemma cpow1x a: \1 c ^c a = \1 c.
Proof.
move: fgraph_set0 domain_set0 => eg de.
by rewrite - (cprod_trivial de) cpow_prod // de /card_prodb /Lg funI_set0.
Qed.

Lemma cpow0x a: a <> \0 c ->\0 c ^c a = \0 c.
Proof.
move=>naz;rewrite/card_pow.
have ->: (functions a \0 c = emptyset).
  apply /set0_P => y /fun_set_P [fy sy tg].
  move: (empty_target_graph fy tg).
  by move: fy => [_ _ dy] ge; case: naz; rewrite - sy dy ge domain_set0.
apply: cardinal_set0.
Qed.

Lemma cpowx2 a: a ^c \2 c = a *c a.
Proof.
rewrite -card_two_pr cpow_sum2 cpowx1c //.
apply: cprod2_pr2; apply: double_cardinal.
Qed.

Definition char_fun A B := Lf (varianti A \1 c \0 c) B (doubleton \1 c \0 c).

Lemma char_fun_axioms A B:
  lf_axiom (varianti A \1 c \0 c) B (doubleton \1 c \0 c).
Proof. move=> z zB; rewrite /varianti;Ytac zA; fprops. Qed.

Lemma char_fun_f A B: function (char_fun A B).
Proof. rewrite/char_fun; apply: lf_function; apply: char_fun_axioms. Qed.

Lemma char_fun_V A B x :
  inc x B -> Vf (char_fun A B) x = (varianti A \1 c \0 c x ).
Proof. move=> xB; rewrite /char_fun; aw; apply: char_fun_axioms. Qed.

Lemma char_fun_V_cardinal A B x:
  inc x B -> cardinalp (Vf (char_fun A B) x).
Proof.
move=> xB; rewrite /char_fun; aw; last by apply: char_fun_axioms.
rewrite /varianti;Ytac h; fprops.
Qed.

Lemma char_fun_V_a A B x: sub A B -> inc x A ->
  Vf (char_fun A B) x = \1 c.
Proof.
move=> AB xA;move: (AB _ xA) => xB; rewrite char_fun_V //.
by apply: varianti_in.
Qed.

Lemma char_fun_V_b A B x: sub A B -> inc x (B -s A) ->
  Vf (char_fun A B) x = \0 c.
Proof.
move=> AB /setC_P [xB nxA]; rewrite char_fun_V //.
by apply: varianti_out.
Qed.

Lemma char_fun_injectiveP A A' B: sub A B -> sub A' B ->
  ((A =A') <-> (char_fun A B = char_fun A' B )).
Proof.
move=> AB A'B; split; first by move => ->.
move=> scf; set_extens x => xs.
  ex_middle u.
  have xc: (inc x (B -s A')) by apply /setC_P; split => //;apply: AB.
  by case: card1_nz; rewrite -(char_fun_V_a AB xs) -(char_fun_V_b A'B xc) scf.
ex_middle u.
have xc: (inc x (B -s A)) by apply /setC_P; split=>// ;apply: A'B.
by case: card1_nz; rewrite -(char_fun_V_a A'B xs) -(char_fun_V_b AB xc) scf.
Qed.

Lemma char_fun_surjective X f: function f -> source f = X ->
  target f = (doubleton \1 c \0 c ) ->
  exists2 A, sub A X & char_fun A X = f.
Proof.
move => fy sy ty.
set W := Zo X (fun z => Vf f z = \1 c).
have WX: sub W X by apply: Zo_S.
exists W => //.
symmetry;rewrite /char_fun; apply: function_exten => //; aw.
apply: char_fun_f.
rewrite sy;move => s sX /=; case: (inc_or_not s W) => ws.
  by rewrite (char_fun_V_a WX ws); move /Zo_P: ws => [].
have wsx: inc s (X -s W) by apply /setC_P.
rewrite - sy in sX; move: (Vf_target fy sX); rewrite ty.
case /set2_P => h; last by rewrite (char_fun_V_b WX wsx).
case: ws; apply:Zo_i => //; ue.
Qed.

Theorem card_setP X: cardinal (powerset X) = \2 c ^c X.
Proof.
rewrite - (cardinal_set2 TP_ne1).
set T := doubleton _ _.
transitivity (card_pow T X); last by apply: cpow_pr; fprops.
rewrite/card_pow; aw.
set K:= functions X T.
apply/card_eqP; exists (Lf (char_fun ^~ X) (powerset X) K); red;aw;split => //.
apply:lf_bijective.
- move => y /setP_P yX; apply /fun_set_P;split => //; rewrite /char_fun; aw.
  by apply /char_fun_f.
- by move => u v /setP_P uX /setP_P vX /(char_fun_injectiveP uX vX).
- move => y /fun_set_P [fy sy ty].
  move: (char_fun_surjective fy sy ty)=> [A pa pb]; exists A => //.
  by apply /setP_P.
Qed.

EIII-3-6 Order relation and operations on cardinals

Definition card_diff a b := cardinal (a -s b).
Notation "x -c y" := (card_diff x y) (at level 50).

Lemma CS_diff a b: cardinalp (a -c b).
Proof. apply CS_cardinal. Qed.

Lemma cardinal_setC A E: sub A E ->
  (cardinal A ) +c (E -c A ) = cardinal E.
Proof.
by move=> AE; rewrite /card_diff csum2_pr2a csum2_pr2b - cardinal_setC2.
Qed.

Lemma cardinal_setC1 a b: b <=c a -> b +c (a -c b ) = a.
Proof.
move=> [cb ca sab].
by rewrite -{1} (card_card cb) cardinal_setC // (card_card ca).
Qed.

Theorem cardinal_le_setCP a b:
  cardinalp a -> cardinalp b ->
  ((b <=c a ) <-> (exists2 c, cardinalp c & b +c c = a )).
Proof.
move=> ca cb; split.
  by exists (cardinal (a -s b)); fprops;apply: cardinal_setC1.
move=> [c cc pbc].
move: (disjointU2_pr3 b c TP_ne1); rewrite pbc.
set b1 := b *s1 _; set d := _ \cup _ => aux.
have bb1: equipotent b1 b by rewrite /b1; eqsym;fprops.
have h1: equipotent_to_subset b1 d by exists b1; fprops; apply: subsetU2l.
apply /cardinal_le_aux2P => //.
apply: (eq_subset_pr2 bb1 (equipotentS aux) h1).
Qed.

Theorem csum_increasing f g:
  domain f = domain g ->
  (forall x, inc x (domain f) -> (Vg f x ) <=c (Vg g x )) ->
  (card_sum f ) <=c (card_sum g ).
Proof.
move=> dfdg ale; apply: sub_smaller => t.
rewrite /disjointU /disjointU_fam.
move /setUb_P; bw; move => [y ydf]; bw.
move /setX_P => [pt Pt /set1_P Qt]; apply/setUb_P; bw; rewrite -dfdg.
ex_tac; bw; rewrite -{2} Qt;apply :setX_i; fprops.
by move: (ale _ ydf) => [_ _];apply.
Qed.

Theorem cprod_increasing f g:
  domain f = domain g ->
  (forall x, inc x (domain f) -> (Vg f x ) <=c (Vg g x )) ->
  (card_prod f ) <=c (card_prod g ).
Proof.
move=> dfdg alle.
by apply: sub_smaller; apply: setXb_monotone1 =>// i /alle [_ _].
Qed.

Lemma csum_increasing1 f j: cardinal_fam f ->
  sub j (domain f) -> (card_sum (restr f j)) <=c (card_sum f ).
Proof.
move=> alc sjd.
apply: sub_smaller => t.
rewrite /disjointU /disjointU_fam.
move /setUb_P; bw; move=> [y yd]; bw => /setX_P [pa pb /set1_P pc].
apply /setUb_P; bw; move: (sjd _ yd) => yf; ex_tac; bw.
apply /setX_P;split => //; rewrite pc; fprops.
Qed.

Lemma cprod_increasing1 f j: cardinal_fam f -> card_nz_fam f ->
  sub j (domain f) -> (card_prod (restr f j)) <=c (card_prod f ).
Proof.
move=> alc alne sjd.
set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) \1 c)).
have fgg: fgraph g by rewrite /g; fprops.
have dgdf : domain g = domain f by rewrite /g; bw.
have cs: (card_prod g = card_prodb j (Vg g)).
  apply: cprod_one_unit=>//; rewrite dgdf //.
  move=> i /setC_P [idf nij]; rewrite /g; bw; rewrite Y_false //.
have drf: domain (restr f j) = j by bw.
have ->: (restr f j = Lg j (Vg g)).
    apply: fgraph_exten; fprops; rewrite! drf; bw=>//.
  move=> x xj; move: (sjd _ xj) => xdf.
  by bw; rewrite /g; bw; Ytac0.
rewrite -/(card_prodb _ _) - cs; apply: cprod_increasing=> //.
move=> x xdg; rewrite /g; bw; try ue.
Ytac h; fprops; apply: card_ge1; [ apply: alc;ue | apply: alne; ue].
Qed.

Lemma csum_Mlele a b a' b':
  a <=c a' -> b <=c b' -> (a +c b ) <=c (a' +c b').
Proof.
move=> aa' bb'; apply: csum_increasing; fprops; bw => x xtp; try_lvariant xtp.
Qed.

Lemma csum_Meqle a b b': b <=c b' -> (a +c b ) <=c (a +c b').
Proof.
move => h; rewrite -(csum2_pr2a a b) -(csum2_pr2a a b').
apply:csum_Mlele;fprops.
Qed.

Lemma csum_Mleeq a b b': b <=c b' -> (b +c a ) <=c (b' +c a ).
Proof. by move => h; rewrite (csumC _ a)(csumC _ a); apply: csum_Meqle. Qed.

Lemma cprod_Mlele a b a' b':
  a <=c a' -> b <=c b' -> (a *c b ) <=c (a' *c b').
Proof.
move=> aa' bb';apply: cprod_increasing;fprops; bw => x xtp; try_lvariant xtp.
Qed.

Lemma csum_M0le a b: cardinalp a -> a <=c (a +c b ).
Proof.
move=> ca.
rewrite -{1}(csum0r ca) - (csum2_pr2b a b).
apply: csum_Meqle; fprops;apply: czero_least.
Qed.

Lemma csum2_pr6 a b: cardinal (a \cup b) <=c a +c b.
Proof.
rewrite - (setU2Cr2 a b) (csum2_pr5 (set_I2Cr b a)) - (csum2_pr2b _ b).
rewrite - (csum2_pr2b a);apply: csum_Meqle;apply: sub_smaller; apply: sub_setC.
Qed.

Lemma cprod_M1le a b: cardinalp a ->
  b <> \0 c -> a <=c (a *c b ).
Proof.
move=> ca nbz.
rewrite -{1}(cprod1r ca) - (cprod2_pr2b a b).
apply: cprod_Mlele; fprops; apply: card_ge1; fprops.
by apply: cardinal_nonemptyset0.
Qed.

Lemma cpow_Mlele a b a' b':
  a <> \0 c -> a <=c a' -> b <=c b' -> (a ^c b ) <=c (a' ^c b').
Proof.
move=> nz aa' bb'.
apply: (@card_leT _ (card_pow a' b)).
  rewrite -2! cpow_pr2.
  rewrite /cst_graph; apply: cprod_increasing; fprops;bw.
  move=> x xb; bw.
move: (cardinal_le_aux1 bb') => [x xb' ebx].
have ->: (a' ^c b = a' ^c x) by apply: cpow_pr; fprops.
rewrite - 2! cpow_pr2 / cst_graph.
rewrite - (restr_Lg (fun _ => a') xb').
apply: cprod_increasing1 =>//; bw.
   red;red; bw;move => t tx; bw; co_tac.
red;bw; move => z zb; bw; dneg a'z; apply: card_leA; first by ue.
apply: czero_least; co_tac.
Qed.

Lemma cpow_M2le x y: x <=c y -> \2 c ^c x <=c \2 c ^c y.
Proof. move=> h; apply: cpow_Mlele; fprops. Qed.

Lemma cpow_Mleeq x y z: x <=c y -> x <> \0 c -> x ^c z <=c y ^c z.
Proof.
move=> xy xz.
have ->: x ^c z = x ^c (cardinal z) by apply cpow_pr; fprops.
have ->: y ^c z = y ^c (cardinal z) by apply cpow_pr; fprops.
apply: cpow_Mlele => //; fprops.
Qed.

Lemma cpow_Meqle0 x a b:
  x <> \0 c -> (cardinal a ) <=c (cardinal b ) ->
  x ^c a <=c x ^c b.
Proof.
move => pa pb.
have -> : x ^c a = (cardinal x) ^c (cardinal a) by apply: cpow_pr; fprops.
have -> : x ^c b = (cardinal x) ^c (cardinal b) by apply: cpow_pr; fprops.
by apply: cpow_Mlele => //; fprops; apply: cardinal_nonemptyset0.
Qed.

Lemma cpow_Meqle x a b:
  x <> \0 c -> a <=c b -> x ^c a <=c x ^c b.
Proof.
move => pa pab; apply cpow_Meqle0 => //.
by rewrite (card_card (proj31 pab)) (card_card (proj32 pab)).
Qed.

Lemma cpow_Mle1 a b:
  cardinalp a -> b <> \0 c -> a <=c (a ^c b ).
Proof.
move=> ca l1b.
case: (equal_or_not a \0 c).
  move => ->; apply: czero_least; fprops.
move=> anz;rewrite - {1} (cpowx1 ca); apply:cpow_Meqle0 => //.
rewrite (card_card CS1); apply: card_ge1; fprops.
by apply: cardinal_nonemptyset0.
Qed.

Theorem cantor a: cardinalp a -> a <c (\2 c ^c a ).
Proof.
move=> ca; rewrite - card_setP.
rewrite - {1} (card_card ca).
split.
  apply /eq_subset_cardP1 /eq_subset_ex_injP.
  exists (Lf (fun x => singleton x) a (powerset a)); red; aw; split => //.
  apply: lf_injective.
    by move=> t ta /=; apply/setP_P => v /set1_P ->.
  by move=> u v ua va; apply: set1_inj.
move; apply/ card_eqP.
move=> [f [[_ suf] sf tf]].
set (X:= Zo a (fun x => (~ inc x (Vf f x)))).
have Xt: (inc X (target f)) by rewrite tf; apply /setP_P; apply: Zo_S.
move: ((proj2 suf) _ Xt) => [y ysf Wy].
have:(~ (inc y X)) by move=> yX; move: (yX) => /Zo_hi;rewrite Wy.
move=> h;case: (h); apply: Zo_i; ue.
Qed.

Lemma infinite_powerset x: infinite_c x -> infinite_c (\2 c ^c x).
Proof.
move => oo; exact (ge_infinite_infinite oo (proj1 (cantor (proj1 oo)))).
Qed.

Lemma cantor_bis: ~ (exists a, forall x, cardinalp x -> inc x a ).
Proof.
move=> [a ap].
set (s:= union a).
set (e:= cardinal s).
have ce: cardinalp e by rewrite /e;fprops.
have le1: (cardinal_le (card_pow card_two e) e).
  set (w:= card_pow card_two e).
  have cw: (cardinalp w) by rewrite /w /card_pow; fprops.
  have sw: (sub w s) by rewrite /s;apply: setU_s1; apply: ap.
  by move: (sub_smaller sw); rewrite -/e (card_card cw).
move: (cantor ce)=> le2;co_tac.
Qed.

Definition succ_c c := Zo (\2 c ^c c) (fun z => cardinal z <=c c).

Lemma succ_cP c: cardinalp c -> forall x,
  (inc x (succ_c c) <-> (ordinalp x /\ cardinal x <=c c )).
Proof.
move => cc x.
move:(cantor cc) => ncc; move: (ncc) => [[_ cc1 _] _]; move: (cc1) => [oc _].
split; first by move /Zo_P =>[h1 h2]; split => //; ord_tac.
move => [h1 h2];apply: Zo_i => //.
move: (card_le_ltT h2 ncc) => h3.
by move /(ordinal_cardinal_le2P cc1 h1): h3 => /ord_ltP0 [].
Qed.

Lemma succ_c_pr1 c (a:= succ_c c): cardinalp c ->
[/\ cardinalp a, c <c a & forall c', c <c c' -> a <=c c'].
Proof.
move => cc.
move: (succ_cP cc) => H.
have ose: ordinal_set a by move => t /H [pa pb].
have oe: ordinalp a.
  apply: ordinal_pr => // t /H [pa pb] s st.
  apply/H; split; first by ord_tac.
  move: (sub_smaller (ordinal_transitive pa st)) => h2; co_tac.
case: (card_le_to_el (CS_cardinal a) cc) => pa.
  by move: (ordinal_irreflexive oe); move /H => []; split.
have pb: forall c', c <c c' -> sub a c'.
  move => c' cc'; move:(proj32_1 cc') => h2.
  move => t /H [sa sb].
  move: (card_le_ltT sb cc').
  by move /(ordinal_cardinal_le2P h2 sa) => /ord_ltP0 [].
have cp: cardinalp a.
  split => // z oz /card_eqP hh; rewrite hh in pa.
  move: (cardinal_ordinal_le oz) => [_ _ s3]; exact: (sub_trans (pb _ pa) s3).
rewrite -{2} (card_card cp); split => //.
by move => c' cc'; split => //; [co_tac | apply: pb].
Qed.

Lemma succ_c_pr4 x y: cardinalp y -> x <c succ_c y -> x <=c y.
Proof.
move => pa pb.
case: (card_le_to_el (proj31_1 pb) pa) => // h.
move: (succ_c_pr1 pa) => [_ _] w; move: (w _ h) => l; co_tac.
Qed.

Lemma CS_succ_c x: cardinalp x -> cardinalp (succ_c x).
Proof. by move=> ic; move: (succ_c_pr1 ic) => []. Qed.

Lemma succ_c_pr2 x: cardinalp x -> x <c succ_c x.
Proof. by move=> ic; move: (succ_c_pr1 ic) => []. Qed.

Lemma succ_c_pr3 x: cardinalp x -> succ_c x <=c \2 c ^c x.
Proof.
move=> ic; move: (succ_c_pr1 ic) => [pa pb]; apply; apply: cantor; co_tac.
Qed.

Lemma succ_c_pr5P x : cardinalp x ->
   forall y, (x <c y <-> succ_c x <=c y).
Proof.
move => cx; split.
  by move => h; move: (proj33 (succ_c_pr1 cx)); apply.
move: (succ_c_pr2 cx) => h1 h2; co_tac.
Qed.

Lemma succ_c_pr4P y: cardinalp y ->
   forall x, (x <c succ_c y <-> x <=c y).
Proof.
move => cy x; split; first by apply: succ_c_pr4.
move => sb; move: (succ_c_pr2 cy) => sc; co_tac.
Qed.

Lemma succ_c_pr6 x y: x <=c y -> succ_c x <=c succ_c y.
Proof.
move => xy.
move: (xy) => [cx cy _].
by apply/succ_c_pr5P => //; apply/succ_c_pr4P.
Qed.

End CardinalOps.
Export CardinalOps.

Module FiniteSets.

EIII-4-1 Definition of integers

Definition Bnat := omega0.

Theorem finite_succP x: cardinalp x ->
  (finite_c (succ x) <-> finite_c x).
Proof.
move=> cx.
case: (finite_dichot cx).
  move => h; rewrite (succ_of_finite h); exact: finite_oP.
by move/infinite_cP => [_ <-].
Qed.

Lemma infinite_Bnat: infinite_set Bnat.
Proof. red; rewrite (card_card CS_omega); exact omega_infinite. Qed.

Lemma BnatP a: inc a Bnat <-> finite_c a.
Proof. exact: omega_P2. Qed.

Lemma Bnat_i a: finite_c a -> inc a Bnat.
Proof. by move /BnatP. Qed.

Lemma Bnat_hi a: inc a Bnat -> finite_c a.
Proof. by move /BnatP. Qed.

Hint Resolve Bnat_i Bnat_hi: fprops.

Lemma BS_succ x: inc x Bnat -> inc (succ x) Bnat.
Proof. move/BnatP => h; apply /BnatP /finite_succP =>// ; fprops. Qed.

Lemma CS_Bnat x: inc x Bnat -> cardinalp x.
Proof. fprops. Qed.

Lemma Bnat_cardinal x: inc x Bnat -> cardinal x = x.
Proof. by move => xB; apply: card_card; apply: CS_Bnat. Qed.

Hint Resolve CS_Bnat : fprops.
Hint Resolve BS_succ: fprops.

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

Lemma succ_of_Bnat n: inc n Bnat -> succ n = succ_o n.
Proof. by move => nb;rewrite succ_of_finite //; apply/BnatP. Qed.

Lemma Bnat_oset x: inc x Bnat -> ordinalp x.
Proof. move => xB;apply: OS_cardinal; fprops. Qed.

Lemma bsum0r x: inc x Bnat -> x +c \0 c = x.
Proof. by move=> xB; apply: csum0r; fprops. Qed.

Lemma bsum0l x: inc x Bnat -> \0 c +c x = x.
Proof. by move=> xB; apply: csum0l; fprops. Qed.

Lemma BS_le_int a b: a <=c b -> inc b Bnat -> inc a Bnat.
Proof. move=> ab /BnatP bi; apply/BnatP; apply: (le_finite_finite bi ab). Qed.

Lemma BS_lt_int a b: a <c b -> inc b Bnat -> inc a Bnat.
Proof. by move => [h _]; apply: (BS_le_int). Qed.

Lemma Bnat_dichot x: cardinalp x -> inc x Bnat \/ infinite_c x.
Proof. by move=> h; case: (finite_dichot h); [ move/BnatP; left | right]. Qed.

Lemma Bnat_le_infinite a b: inc a Bnat -> infinite_c b -> a <=c b.
Proof. by move/BnatP; apply finite_le_infinite. Qed.

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

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

Lemma BS0: inc \0 c Bnat.
Proof. apply: Bnat_i; apply: finite_zero. Qed.

Lemma BS1: inc \1 c Bnat.
Proof. move: BS0; rewrite - succ_zero; fprops. Qed.

Lemma BS2: inc \2 c Bnat.
Proof. move: BS1; rewrite - succ_one; fprops. Qed.

Lemma BS3: inc \3 c Bnat.
Proof. move: BS2; rewrite /card_three; fprops. Qed.

Lemma BS4: inc \4 c Bnat.
Proof. move: BS3; rewrite /card_four; fprops. Qed.

Hint Resolve BS0 BS1 BS2: fprops.

Lemma finite_0: finite_c \0 c.
Proof. fprops. Qed.

Lemma finite_1: finite_c \1 c.
Proof. fprops. Qed.

Lemma finite_2: finite_c \2 c.
Proof. fprops. Qed.

Hint Resolve finite_0 finite_1 finite_2 : fprops.

Lemma two_plus_two: \2 c +c \2 c = \4 c.
Proof.
rewrite /card_four (Bsucc_rw BS3).
rewrite /card_three (Bsucc_rw BS2).
rewrite - csumA - card_two_pr //.
Qed.

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

Lemma power_2_4: \2 c ^c \4 c = \4 c ^c \2 c.
Proof.
by rewrite -{2} two_times_two cpow_prod2 -two_plus_two cpow_sum2.
Qed.

Lemma card_le_succ0 a: cardinalp a -> a <=c (succ a ).
Proof. by move=> ca; rewrite card_succ_pr4 //; apply: csum_M0le. Qed.

Lemma Bnat_in_sum a b: cardinalp b ->
  inc (a +c b) Bnat ->inc b Bnat.
Proof.
move=> cb /BnatP /finite_cP [cp fcp]; apply /BnatP /finite_cP;split=>//.
move: fcp; rewrite (card_succ_pr4 cb) (card_succ_pr4 cp) - csumA.
by move => h1 h2; case: h1; rewrite - h2.
Qed.

Lemma Bnat_in_sum2 a b: cardinalp a ->
  inc (a +c b) Bnat ->inc a Bnat.
Proof. rewrite csumC => ca; apply: (Bnat_in_sum ca). Qed.

Lemma Bnat_in_product a b: cardinalp a ->
  b <> \0 c -> inc (a *c b) Bnat -> inc a Bnat.
Proof.
move=> ca nzb.
have on: (\1 c <=c (cardinal b)).
  apply: card_ge1; [fprops | by apply: cardinal_nonemptyset0].
rewrite -(cprod2_pr2b a b) -(cardinal_setC1 on) cprod_sumDl cprod1r //.
apply: (Bnat_in_sum2 ca).
Qed.

Lemma BS_nsucc x: cardinalp x -> inc (succ x) Bnat -> inc x Bnat.
Proof.
by move=> xs sB; case: (Bnat_dichot xs)=> // /infinite_cP [_] ->.
Qed.

Lemma cdiff_le1 a b: inc a Bnat -> a -c b <=c a.
Proof.
move => /Bnat_cardinal h.
by move: (sub_smaller (@sub_setC a b)); rewrite h.
Qed.

Lemma BS_diff a b: inc a Bnat -> inc (a -c b) Bnat.
Proof.
move => h; apply:(BS_le_int (cdiff_le1 b h) h).
Qed.

Hint Resolve BS_diff: fprops.

Definition cpred := union.

Lemma cpred_pr n: inc n Bnat -> n <> \0 c ->
  (inc (cpred n) Bnat /\ n = succ (cpred n)).
Proof.
move/BnatP ; rewrite /finite_c finite_succ => p1 p2.
case: p1; first by move=> aux; case: p2 =>//.
move=> [y fy ns].
move: (succo_K (proj1 fy)).
rewrite /cpred;rewrite -ns; move => ->.
by rewrite (succ_of_finite fy);split; fprops.
Qed.

Lemma card_le_succ a: inc a Bnat -> a <=c (succ a ).
Proof. move=> aB; apply: card_le_succ0; fprops. Qed.

Lemma card_lt_succ a: inc a Bnat -> a <c (succ a ).
Proof.
move=> aB; split; first by apply: card_le_succ.
by move: aB => /BnatP /finite_cP [h].
Qed.

Hint Resolve card_le_succ card_lt_succ: fprops.

Lemma cdiff_nz a b: b <c a -> (a -c b ) <> \0 c.
Proof.
move => [ leba neba] cs.
move: (cardinal_setC1 leba); rewrite cs csum0r//; co_tac.
Qed.

Theorem card_lt_succ_leP n: inc n Bnat -> forall a,
  (a <c (succ n ) <-> a <=c n).
Proof.
move=> fn; split; last by move: (card_lt_succ fn)=> p1 p2; co_tac.
move: (BS_succ fn) => sn ltas; move: (ltas) => [leas nas].
move: (BS_diff a sn) (cardinal_setC1 leas) (cdiff_nz ltas).
set c := (_ -c a) => cB pac nzc.
move: (cpred_pr cB nzc)=> [cp pv].
move: pac; rewrite pv (Bsucc_rw cp) csumA (Bsucc_rw fn) => h.
have <-: (a +c (cpred c) = n) by apply: succ_injective; fprops.
apply: csum_M0le; co_tac.
Qed.

Lemma card_le_succ_succP a b: cardinalp a -> cardinalp b ->
  (a <=c b <-> succ a <=c succ b).
Proof.
move => ca cb; split => h.
  rewrite ! card_succ_pr4 //.
  apply: (csum_Mlele h (card_leR CS1)).
case: (Bnat_dichot cb) => fb; last first.
    move /infinite_cP : (fb) => [_ e1]; rewrite -e1 in h.
    case: (Bnat_dichot ca) => fa; first by apply: Bnat_le_infinite.
  by move /infinite_cP : (fa) => [_ ->].
apply/(card_lt_succ_leP fb).
move: (card_le_succ0 ca) => le1.
split; first by apply: (card_leT le1 h).
move=> aux; rewrite -aux in h.
move: (BS_succ fb).
rewrite -aux; move /BnatP /finite_cP => [_]; case; co_tac.
Qed.

Lemma cpred_pr1 n: cardinalp n -> cpred (succ n) = n.
Proof.
move=> cn.
case: (finite_dichot cn).
  move: cn => [cn _] h; by rewrite succ_of_finite //;apply: succo_K.
move => ifn; move: (ifn) => /infinite_cP [_ <-].
apply: (infinite_card_limit1 ifn).
Qed.

Lemma cpred_pr2 n: inc n Bnat -> cpred (succ n) = n.
Proof. move=> nb; apply: cpred_pr1; fprops. Qed.

Lemma cpred_pr3 n: inc n Bnat ->
  n = \0 c \/ exists2 m, inc m Bnat & n = succ m.
Proof.
move=> nB; case: (equal_or_not n card_zero); first by left.
by move /(cpred_pr nB) => [pa pb];right; exists (cpred n).
Qed.

Lemma card_le_succ_lt0P a b: cardinalp a -> inc b Bnat ->
  (succ a <=c b <-> a <c b).
Proof.
move=> ca fb; symmetry.
case: (equal_or_not b card_zero).
  move=> ->; split => h; first by case: (card_lt0 h).
  have lts:(cardinal_lt (succ a) \0 c) by split=>//; apply: succ_nz.
  case: (card_lt0 lts).
move=> nzb; move: (cpred_pr fb nzb)=> [pb ->].
apply: (iff_trans (card_lt_succ_leP pb a)).
apply:(card_le_succ_succP ca); fprops.
Qed.

Lemma card_le_succ_ltP a b: inc a Bnat ->
  (succ a <=c b <-> a <c b).
Proof.
move=> aB.
have ca: cardinalp a by fprops.
have fa: finite_c a by fprops.
split => h; have cb: cardinalp b by co_tac.
  case: (finite_dichot cb).
    by move => fb; apply/card_le_succ_lt0P; fprops.
  by apply:finite_lt_infinite.
case: (finite_dichot cb).
  by move => fb; apply/card_le_succ_lt0P; fprops.
by move => h1; apply:finite_le_infinite => //; apply/finite_succP.
Qed.

Lemma card_succ_succ_ltP n m: inc n Bnat -> inc m Bnat ->
  ((succ n <c succ m ) <-> (n <c m )).
Proof.
move => nB mB.
exact:(iff_trans (card_lt_succ_leP mB (succ n)) (card_le_succ_ltP m nB)).
Qed.

Lemma card_finite_setP x: finite_set x <-> inc (cardinal x) Bnat.
Proof. apply: iff_sym;apply:BnatP. Qed.

Lemma emptyset_finite: finite_set emptyset.
Proof. apply /card_finite_setP; rewrite cardinal_set0 ; apply: BS0. Qed.

Lemma strict_sub_smaller x y: ssub x y -> finite_set y ->
  (cardinal x ) <c (cardinal y ).
Proof.
move=> ssxy fsy.
move: (setC_ne ssxy) =>[u uc].
set (z:= y -s1 u).
have ->: (cardinal y = succ (cardinal z)).
  by rewrite /z - card_succ_pr1 setC1_K //; move /setC_P : uc => [].
move: ssxy => [sxy _].
have szy: sub z y by rewrite /z; apply: sub_setC.
have: sub x z.
   move=> t tx; apply /setC1_P; split; [ by apply: sxy | move => tu].
   move/setC_P: uc => [_]; case; ue.
move /sub_smaller => lexz.
apply /card_lt_succ_leP => //; apply /BnatP; apply: (sub_finite_set szy fsy).
Qed.

Lemma strict_sub_smaller1 y:
  (forall x, ssub x y -> (cardinal x ) <c (cardinal y )) <->
  finite_set y.
Proof.
split; last by move => fsy x ss; apply: strict_sub_smaller.
move=> h.
case: (emptyset_dichot y); first by move => ->; apply: emptyset_finite.
move=> [u uy].
set (z:=complement y (singleton u)).
have ssy: ssub z y.
  split; first by apply: sub_setC.
  by move=> ezy; move: uy; rewrite -ezy; move /setC1_P => [_].
have yt: y = z +s1 u by rewrite setC1_K.
move: (card_succ_pr1 y u); rewrite -/z -yt => cy.
have cc: cardinalp (cardinal z) by fprops.
red; rewrite cy.
apply /finite_succP => //; apply /finite_cP;split => //.
by move: (h _ ssy) => [_ ]; rewrite cy.
Qed.

Lemma range_smaller_cardinal f:
  fgraph f -> cardinal (range f) <=c cardinal (domain f).
Proof.
move=> fgf.
have ff: (function (triple (domain f) (range f) f)).
  by apply: function_pr; fprops.
have ->: (range f = image_of_fun (triple (domain f)(range f) f)).
  by rewrite (image_by_fun_source ff); aw.
move:(image_smaller_cardinal ff); aw.
Qed.

Lemma finite_range f: fgraph f -> finite_set (domain f) ->
  finite_set (range f).
Proof.
move=> /range_smaller_cardinal => pa pb; apply :(le_finite_finite pb pa).
Qed.

Lemma finite_image f: function f -> finite_set (source f) ->
  finite_set (image_of_fun f).
Proof.
move=> ff fs; move: (image_smaller_cardinal ff)=> cle.
apply: (le_finite_finite fs cle).
Qed.

Lemma finite_image_by f A: function f -> sub A (source f) ->
  finite_set A -> finite_set (image_by_fun f A).
Proof.
move=> ff sAsf fsA.
set (g:= restriction1 f A).
have sg: (surjection g) by rewrite /g; apply: restriction1_fs.
have <-:(image_of_fun g = image_by_fun f A).
   rewrite surjective_pr0 /g /restriction1; aw.
apply: finite_image=>//; first by fct_tac.
rewrite /g/restriction1; aw.
Qed.

Lemma finite_fun_image a f: finite_set a ->
  finite_set (fun_image a f).
Proof.
move=> fsa;move: (fun_image_smaller a f) => h.
apply: (le_finite_finite fsa h).
Qed.

Lemma equipotent_domain f: fgraph f -> domain f \Eq f.
Proof.
move => h.
exists (Lf (fun z => J z (Vg f z)) (domain f) f); red;aw;split => //.
apply: lf_bijective.
    by apply: fdomain_pr1.
  by move => u v _ _ /pr1_def.
move => y yf; rewrite (in_graph_V h yf); exists (P y); fprops.
Qed.

Lemma finite_graph_domain f: fgraph f ->
  (finite_set f <-> finite_set (domain f)).
Proof.
by move=> /equipotent_domain /card_eqP; rewrite /finite_set /finite_c => ->.
Qed.

Lemma bijective_if_same_finite_c_inj f:
  cardinal (source f) = cardinal (target f) -> finite_set (source f) ->
  injection f -> bijection f.
Proof.
move=> csftf fs injf; split=>//; apply: surjective_pr1; first by fct_tac.
have fst: (finite_set (target f)) by red; ue.
have sit: (sub (image_of_fun f) (target f)).
  apply: fun_image_Starget; fct_tac.
ex_middle it.
move:(strict_sub_smaller (conj sit it) fst) => [cle ne].
case: ne; transitivity (cardinal (source f))=>//.
symmetry; apply /card_eqP.
exists (restriction_to_image f); red.
rewrite {2 3} /restriction_to_image /restriction2; aw.
split => //; by apply: (restriction_to_image_fb injf).
Qed.

Lemma bijective_if_same_finite_c_surj f:
  cardinal (source f) = cardinal (target f) -> finite_set (source f) ->
  surjection f -> bijection f.
Proof.
move=> cstf fsf sf.
move: (exists_right_inv_from_surj sf)=> [g rig].
move: (right_i_source rig) =>sg.
move: (right_inverse_fi 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.
have bg :=(bijective_if_same_finite_c_inj csftf fss ig).
have bc: (bijection (compose f g)) by rewrite c; apply: identity_fb.
apply: (left_compose_fb co bc bg).
Qed.

EIII-6-1 The set of natural integers

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 60).
Notation "x <N y" := (Bnat_lt x y) (at level 60).

Lemma Bnat_order_wor: worder_on Bnat_order Bnat.
Proof. by move: (wordering_cardinal_le_pr CS_Bnat). Qed.

Lemma Bnat_order_leP x y:
  gle Bnat_order x y <-> x <=N y.
Proof. apply: graph_on_P1. Qed.

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

Lemma least_int_prop (prop:property):
  (forall x, prop x -> inc x Bnat) -> (exists x, prop x) ->
  prop \0 c \/ (exists x, [/\ inc x Bnat, prop (succ x) & ~ prop x]).
Proof.
move=> pi [x xp].
set (X:=Zo Bnat prop).
have sX: sub X Bnat by apply: Zo_S.
have nX: nonempty X by exists x; apply: Zo_i=>//; apply: pi.
case: (Bnat_wordered sX nX)=> q.
   by left; move: q =>/Zo_hi.
right; move: q=> [a [aB /Zo_hi psa /Zo_P h]].
by exists a; split => //; dneg h1.
Qed.

Lemma least_int_prop1 (prop:property):
  (forall x, prop x -> inc x Bnat) -> ~(prop \0 c ) ->
  (exists x, prop x) -> (exists x, [/\ inc x Bnat, prop(succ x) & ~ prop x]).
Proof.
move=> alp npz exp; case: (least_int_prop alp exp)=>// h.
Qed.

Lemma least_int_prop2 (prop:property):
    (prop \0 c) -> (exists2 x, inc x Bnat & ~ prop x) ->
    (exists x, [/\ inc x Bnat, prop x & ~ prop(succ x)]).
Proof.
move => qa [y r1 r2].
pose q n := inc n Bnat /\ ~ prop n.
have pa: (forall x, q x -> inc x Bnat) by move => x;case.
have pb: ~ q \0 c by case.
have pc: exists x, q x by exists y.
move: (least_int_prop1 pa pb pc) => [x [ra [_ rb] rc]]; exists x;split => //.
by ex_middle np; case: rc; split.
Qed.

Section BnatIinterval.
Variables (a b: Set).
Hypotheses (ab: inc a Bnat) (bB: inc b Bnat).

Lemma Bint_ccP x:
  (inc x (interval_cc Bnat_order a b) <-> (a <=N x /\ x <=N b )).
Proof.
rewrite /interval_cc (proj2 Bnat_order_wor); split.
  by move /Zo_P => [xb [/Bnat_order_leP pa /Bnat_order_leP pb]].
move => [pa pb]; apply /Zo_i; first by move: pa => [_].
by split; apply /Bnat_order_leP.
Qed.

Lemma Bint_coP x:
  (inc x (interval_co Bnat_order a b) <-> (a <=N x /\ x <N b )).
Proof.
rewrite/ Bnat_lt/interval_co (proj2 Bnat_order_wor); split.
  by move /Zo_P => [xb []] /Bnat_order_leP pa [] /Bnat_order_leP pb xnb.
move => [pa [pb pc]]; apply /Zo_i; first by move: pa => [_].
by split; [| split => // ];apply /Bnat_order_leP.
Qed.

Lemma Bint_ccP1 x:
  (inc x (interval_cc Bnat_order a b) <-> (a <=c x /\ x <=c b )).
Proof.
apply (iff_trans (Bint_ccP x)); split.
   by move=> [[_ _ pa] [_ _ pb]].
move=> [ax bx].
have xB: inc x Bnat by Bnat_tac.
done.
Qed.

Lemma Bint_coP1 x:
  (inc x (interval_co Bnat_order a b) <-> (a <=c x /\ x <c b )).
Proof.
apply (iff_trans (Bint_coP x)); split.
  by move=> [[_ _ pa] [[_ _ pb] pc]].
move=> [ax [bx xb]].
have xB //: inc x Bnat by Bnat_tac.
Qed.

End BnatIinterval.

EIII-4-3 The principle of induction

Lemma cardinal_c_induction (r:property):
  (r \0 c) -> (forall n, inc n Bnat-> r n -> r (succ n))
  -> (forall n, inc n Bnat -> r n).
Proof.
move=> r0 ri n nN.
ex_middle nrn.
have pa: (exists2 x, inc x Bnat & ~ r x) by exists n.
by move: (least_int_prop2 r0 pa) => [x [pb pc]]; case; apply: ri.
Qed.

Lemma cardinal_c_induction1 (r:property):
  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=> s si n nB; apply: (si)=>//.
ex_middle nrn.
apply: cardinal_c_induction=>//.
  rewrite /s=> p f0 fp np; case: (card_lt0 np).
move=> m fm sm p fsp fp lp.
case: (equal_or_not p m); first by move=>->; apply: si =>//.
by move=> pm; apply: sm=>//; split=>//; move: lp => /(card_lt_succ_leP fm).
Qed.

Lemma cardinal_c_induction2 (r:property) 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=> fk rk ri n fn kn.
move: n fn kn; apply: cardinal_c_induction.
  by move=> h; rewrite - (card_le0 h).
move=> m fm sm; case: (equal_or_not k (succ m)); first by move => <-.
move => ks ksm; have: k <c (succ m) by split.
move/(card_lt_succ_leP fm) => lekm.
by apply: ri=>//; apply: sm.
Qed.

Lemma cardinal_c_induction3 (r:property) 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=> 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 -(card_le0 az).
move=> m fm sm am; move/(card_le_succ_ltP _ fm) => mb.
case: (equal_or_not a (succ m)); first by move => <-.
move=> asm; have: a <c (succ m) by split.
move/(card_lt_succ_leP fm) => leam.
apply: ri=>//;apply: sm => //; by move: mb=> [mb _].
Qed.

Lemma cardinal_c_induction4 (r:property) 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=> 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 (r:property) 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=> 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; apply /Bint_coP1.
move/(Bint_ccP1 aB bB) => [am mb].
apply: (cardinal_c_induction3 aB bB)=>//.
Qed.

Lemma setU1_finite X x:
  finite_set X -> finite_set (X +s1 x).
Proof.
move=>fX; case: (inc_or_not x X) => h; first by rewrite (setU1_eq h).
red; rewrite card_succ_pr //; apply /finite_succP; fprops.
Qed.

Lemma set1_finite x: finite_set(singleton x).
Proof.
apply/ card_finite_setP; rewrite cardinal_set1; apply: BS1.
Qed.

Lemma set2_finite x y: finite_set(doubleton x y).
Proof.
have ->: (doubleton x y = (singleton x) +s1 y) by symmetry;apply: setU2_11.
apply: setU1_finite; apply: set1_finite.
Qed.

Lemma finite_set_scdo: finite_set (substrate canonical_doubleton_order).
Proof.
rewrite (proj2 cdo_wor); apply: set2_finite.
Qed.

Lemma setU1_succ_card x n: cardinalp n -> cardinal x = succ n ->
  exists u v, [/\ x = u +s1 v, ~(inc v u ) & cardinal u = n].
Proof.
move=> cn cx.
case: (emptyset_dichot x) => h.
  move: cx;rewrite h cardinal_set0 =>h'.
  symmetry in h'; case: (succ_nz h').
move: h=> [y yx].
move: (setC1_K yx) => xt.
exists (x -s1 y); exists y;split =>//;first by apply: setC1_1.
apply: succ_injective1; fprops.
by rewrite - cx -xt (card_succ_pr1 x y) xt.
Qed.

Lemma finite_set_induction0 (s:property):
  s emptyset -> (forall a b, s (a) -> ~(inc b a ) -> s (a +s1 b)) ->
  forall x, finite_set x -> s x.
Proof.
move=> se si x /card_finite_setP fx.
pose r n := forall x, cardinal x = n -> s x.
apply: (cardinal_c_induction (r:= r) _ _ fx); last by [].
  by rewrite /r => y h; rewrite (cardinal_nonemptyset h).
move=> n fn rn.
have cn: (cardinalp n) by fprops.
move=> y yp; move: (setU1_succ_card cn yp) => [u [v [yt nvu cu]]].
by rewrite yt; apply: si=>//; apply: rn.
Qed.

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

Lemma finite_set_induction1 (A B:property) x:
  (A emptyset -> B emptyset)
  -> (forall a b, (A a -> B a) -> A(a +s1 b) -> B(a +s1 b))
  -> finite_set x -> A x -> B x.
Proof.
move=> h1 h2 fs.
by pose s x := A x -> B x; apply: (finite_set_induction (s:=s) h1).
Qed.

Lemma finite_set_induction2 (A B:property) x:
  (forall a, A (singleton a) -> B (singleton a))
  -> (forall a b, (A a -> nonempty a -> B a) ->
    nonempty a -> A(a +s1 b) -> B(a +s1 b))
  -> finite_set x -> A x -> nonempty x -> B x.
Proof.
move=> fA fr.
pose s x := A x -> nonempty x -> B x.
apply: (finite_set_induction (s:=s)).
  by rewrite /s; move=> _ [t /in_set0].
move=> a b sa.
case: (emptyset_dichot a) => pa.
  have ->: (a +s1 b = singleton b) by rewrite pa; exact: set0_U2.
  by move => h _; apply: fA.
by move=> h h'; apply: fr.
Qed.

Lemma csum_via_succ' a b: cardinalp b ->
  a +c (succ b ) = succ (a +c b).
Proof.
move => cb; rewrite (card_succ_pr4 cb) csumA (card_succ_pr4) //; fprops.
Qed.

Lemma cprod_via_sum' a b: cardinalp b ->
  a *c (succ b ) = (a *c b ) +c a.
Proof.
move=> bB; rewrite (card_succ_pr4 bB) cprod_sumDl.
rewrite - (csum2_pr2b (a *c b) a) - (cprod1l (CS_cardinal a)).
by rewrite (cprod2_pr2b \1 c a) (cprodC \1 c).
Qed.

Lemma pow_succ' a b: cardinalp b ->
  a ^c (succ b ) = (a ^c b ) *c a.
Proof.
move=> bB; rewrite (card_succ_pr4 bB) cpow_sum2.
rewrite (cpowx1c a); apply: cprod2_pr2 => //; apply: double_cardinal.
Qed.

Lemma csum_via_succ a b: inc b Bnat ->
  a +c (succ b ) = succ (a +c b).
Proof. move => /CS_Bnat; apply: csum_via_succ'. Qed.

Lemma csum_via_succ1 a b: inc a Bnat ->
   (succ a ) +c b = succ (a +c b).
Proof. by move=> aB; rewrite csumC (csum_via_succ _ aB) csumC. Qed.

Lemma cprod_via_sum a b: inc b Bnat -> a *c (succ b ) = (a *c b ) +c a.
Proof. move => /CS_Bnat; apply: cprod_via_sum'. Qed.

Lemma pow_succ a b: inc b Bnat ->
  a ^c (succ b ) = (a ^c b ) *c a.
Proof. move => /CS_Bnat; apply: pow_succ'. Qed.

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

Lemma BS_prod: 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; first by rewrite cprod0r; fprops.
by move=> n nB mB; rewrite cprod_via_sum; fprops; apply: BS_sum.
Qed.

Lemma BS_pow a b: inc a Bnat -> inc b Bnat ->
  inc (a ^c b) Bnat.
Proof.
move=> aB bB.
move: b bB; apply: cardinal_c_induction; first by rewrite cpowx0; fprops.
by move=> n nB mB; rewrite pow_succ => //;apply: BS_prod.
Qed.

Lemma BS_pow2 n: inc n Bnat -> inc (\2 c ^c n) Bnat.
Proof. apply: BS_pow; fprops. Qed.

Hint Resolve BS_sum BS_prod: fprops.
Hint Resolve BS_pow BS_pow2: fprops.

Lemma finite_prod2 u v:
   finite_set u -> finite_set v -> finite_set (u \times v).
Proof.
move =>/card_finite_setP ha /card_finite_setP hb.
apply /card_finite_setP; rewrite - cprod2_pr1 - cprod2_pr2a - cprod2_pr2b.
fprops.
Qed.

EIII-4-4 Finite subsets of ordered sets

Lemma finite_set_induction3 (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 (a +s1 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=> 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 apply: p1.
move=> a b p4 nea st.
have saE: sub a E by apply: sub_trans st; 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 r X:
  right_directed r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> bounded_above r X.
Proof.
move=> [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 _ (set2_1 x b)) => xy.
  move: (upy _ (set2_2 x b)) => lby.
  move=> t /setU1_P; 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 r X:
  lattice r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, greatest_lower_bound r X x.
Proof.
move=> [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.
   move /(glbP or asr)=> [[xsr lb] glex].
  have st: sub (a +s1 b) (substrate r) by apply: setU1_sub.
  have sd: sub (doubleton x b) (substrate r) by apply: sub_set2.
  move=> /(glbP or sd) [[ysr lby] lgley].
  move: (lby _ (set2_1 x b)) => xy.
  move: (lby _ (set2_2 x b)) => lbyy.
  apply /(glbP or st); split.
    split =>// z /setU1_P; case; last by move=> ->.
    move=>za; move: (lb _ za)=> xa; order_tac.
  move=> z [ze xx].
  apply: lgley; split=>//; move=> t /set2_P [] ->.
    apply: glex; split=>//.
    move=> u ua; apply: xx; fprops.
  apply: xx; fprops.
by move=> Z x Zr _ /(glbP or Zr) [[xsr _] _].
Qed.

Lemma finite_subset_lattice_sup r X:
  lattice r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, least_upper_bound r X x.
Proof.
move=> [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.
  move /(lubP or asr)=> [[xsr lb] glex].
  have st: sub (a +s1 b) (substrate r) by apply: setU1_sub.
  have sd: sub (doubleton x b) (substrate r) by apply: sub_set2.
  move=> /(lubP or sd) [[ysr lby] lgley].
  move: (lby _ (set2_1 x b)) => xy.
  move: (lby _ (set2_2 x b)) => lbyy.
  apply /(lubP or st); split.
    split =>// z /setU1_P; case; last by move=> ->.
    move=>za; move: (lb _ za)=> xa; order_tac.
  move=> z [ze xx].
  apply: lgley; split=>//; move=> t /set2_P [] ->.
    apply: glex; split=>//.
    move=> u ua; apply: xx; fprops.
  apply: xx; fprops.
by move=> Z x Zr _ /(lubP or Zr) [[xsr _] _].
Qed.

Lemma finite_subset_torder_greatest r X:
  total_order r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, greatest (induced_order r X) x.
Proof.
move=> [or tor] fsX Xsr neX.
move: neX fsX Xsr.
apply: (finite_set_induction3
  (p:=fun X x => greatest (induced_order r X) x)) => //.
    move=> a b asr bsr.
    have sd: sub (doubleton a b) (substrate r) by apply: sub_set2.
    by case: (tor _ _ asr bsr)=> cp; [exists b | exists a]; red; aw; split;
     fprops; move=> x /set2_P [] ->; apply/iorder_gleP; fprops; order_tac.
  move=> a b x y asr bsr;rewrite /greatest.
  have sta: (sub (a +s1 b) (substrate r)) by apply: setU1_sub.
  rewrite iorder_sr //; move=> [xa xp].
  move: (asr _ xa) => xsr.
  have sd: sub (doubleton x b) (substrate r) by apply: sub_set2.
  move: xp; aw; move=> xp [yd yp]; split.
    move: yd => /set2_P []->; fprops.
  move: (iorder_gle1 (yp _ (set2_1 x b))) => xy.
  move: (iorder_gle1 (yp _ (set2_2 x b)))=> lby.
  have yt: inc y (a +s1 b) by case /set2_P: yd => ->; fprops.
  move=> z zi; apply /iorder_gleP => //.
  case /setU1_P: zi => h; last by ue.
  move:(iorder_gle1 (xp _ h)) => zx; order_tac.
move=> Z x Zs neZ [h gex]; apply: (Zs).
move: h; aw.
Qed.

Lemma finite_subset_torder_least r X:
  total_order r ->finite_set X -> sub X (substrate r) -> nonempty X
  -> exists x, least (induced_order r X) x.
Proof.
move=> tor fsX Xsr neX.
have or: order r by move: tor=> [].
move: (total_order_opposite tor)=> rtor.
move: (opp_osr or) => [aa so]; move: (Xsr); rewrite - so => rXsr.
move: (finite_subset_torder_greatest rtor fsX rXsr neX)=> [x []]; aw; fprops.
move=> xX xg; exists x; red;aw;split => //.
move=> a aX; move: (iorder_gle1 (xg _ aX)) => /igraph_pP h.
by apply /iorder_gleP.
Qed.

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

Lemma finite_set_torder_least r:
  total_order r ->finite_set (substrate r) -> nonempty (substrate r)
  -> exists x, least r x.
Proof.
move=> tor fss nes; move: (tor)=> [or _].
rewrite - (iorder_substrate or).
apply: finite_subset_torder_least; fprops.
Qed.

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

Lemma finite_subset_Bnat X: sub X Bnat -> finite_set X -> nonempty X ->
   exists2 n, inc n X & forall m, inc m X -> m <=c n.
Proof.
move => pa pb pc.
move: Bnat_order_wor => [wor sr].
have pd: sub X (substrate Bnat_order) by rewrite sr.
move: (finite_subset_torder_greatest (worder_total wor) pb pd pc).
move => [n []]; rewrite (iorder_sr (proj1 wor) pd) => pe pf; ex_tac.
by move => m /pf /iorder_gle1 /Bnat_order_leP [].
Qed.

Lemma finite_set_maximal r:
  order r ->finite_set (substrate r) -> nonempty (substrate r) ->
  exists x, maximal r x.
Proof.
move=> 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; exact (iorder_gle1 (xge _ yX)).
Qed.

Section LatticeProps.

Variable (r: Set).
Hypothesis lr: lattice r.
Let E := substrate r.

Lemma lattice_finite_sup2 x:
  finite_set x -> sub x E -> nonempty x -> has_supremum r x.
Proof.
apply: (finite_set_induction2 (A:=fun x => (sub x (substrate r)))).
  move => a asr;rewrite -/(singleton a).
  have ar: inc a (substrate r) by apply: asr; fprops.
  by move: lr => [or lr1]; move: (lr1 _ _ ar ar) =>[p1 p2].
move=> a b xx yy zz.
have p1: sub a (substrate r) by apply: sub_trans zz; fprops.
have p2: (inc b (substrate r)) by apply: zz; fprops.
move: (xx p1 yy)=> [c cs].
exists (sup r c b).
apply: (lattice_finite_sup1 lr p1 cs p2).
Qed.

Lemma lattice_finite_inf2 x:
  finite_set x -> sub x E -> nonempty x -> has_infimum r x.
Proof.
apply: (finite_set_induction2 (A:=fun x => (sub x (substrate r)))).
  move => a asr;rewrite -/(singleton a).
  have ar: inc a (substrate r) by apply: asr; fprops.
  by move: lr => [or lr1]; move: (lr1 _ _ ar ar) =>[p1 p2].
move=> a b xx yy zz.
have p1: sub a (substrate r) by apply: sub_trans zz; fprops.
have p2: (inc b (substrate r)) by apply: zz; fprops.
move: (xx p1 yy)=> [c cs].
exists (inf r c b); apply: (lattice_finite_inf1 lr p1 cs p2).
Qed.

Lemma lattice_finite_sup3P x y:
  finite_set x -> nonempty x -> sub x E ->
  (gle r (supremum r x) y <-> (forall z, inc z x -> gle r z y )).
Proof.
move=> fsx nex xsr.
move: (lattice_finite_sup2 fsx xsr nex) => hs.
have or: order r by move: lr => [ok _].
move: (supremum_pr or xsr hs) => [[p1 p2] p3]; split.
  move=> p4 z zx; move: (p2 _ zx) => p5; order_tac.
move=> p4; apply: p3; split => //.
move: nex=> [u ux]; move: (p4 _ ux) => p5; order_tac.
Qed.

Lemma lattice_finite_inf3P x y:
  finite_set x -> nonempty x -> sub x E ->
  (gle r y (infimum r x) <-> (forall z, inc z x -> gle r y z )).
Proof.
move=> fsx nex xsr.
move: (lattice_finite_inf2 fsx xsr nex) => hs.
have or: order r by move: lr => [ok _].
move: (infimum_pr or xsr hs) => [[p1 p2] p3]; split.
  move=> p4 z zx; move: (p2 _ zx) => p5; order_tac.
move=> p4; apply: p3; split => //.
move: nex=> [u ux]; move: (p4 _ ux) => p5; order_tac.
Qed.

Lemma supremum_setU1 a b:
  sub a E -> has_supremum r a -> inc b E ->
  supremum r (a +s1 b) = sup r (supremum r a) b.
Proof.
move=> asr hsa bsr; move: lr => [or _]; symmetry; apply: supremum_pr2 =>//.
by apply: lattice_finite_sup1 => //;apply: supremum_pr1.
Qed.

Lemma infimum_setU1 a b:
  sub a E -> has_infimum r a -> inc b E ->
  infimum r (a +s1 b) = inf r (infimum r a) b.
Proof.
move: lr => [or _]; move=> asr hsa bsr; symmetry; apply: infimum_pr2 => //.
by apply: lattice_finite_inf1 => //;apply: infimum_pr1.
Qed.

Lemma sup_setU1 X a:
   sub X E -> nonempty X -> finite_set X ->
   inc a E -> supremum r (X +s1 a) = sup r (supremum r X) a.
Proof.
move => pb pc pd pe; apply:supremum_setU1 => //.
by apply: lattice_finite_sup2.
Qed.

Lemma inf_setU1 X a:
   sub X E -> nonempty X -> finite_set X ->
   inc a E -> infimum r (X +s1 a) = inf r (infimum r X) a.
Proof.
move => pb pc pd pe; apply:infimum_setU1 => //.
by apply: lattice_finite_inf2.
Qed.

End LatticeProps.

EIII-4-5 Properties of finite character

Definition finite_character s:=
  forall x, (inc x s ) <-> (forall y, (sub y x /\ finite_set y) -> inc y s ).

Lemma finite_character_example r: order r ->
  finite_character(Zo (powerset (substrate r)) (fun z =>
    total_order (induced_order r z))).
Proof.
move=> or s; split.
  move /Zo_P => [] /setP_P => [sr tor] y [ys fsy];apply: Zo_i.
  have sys: (sub y (substrate r)) by apply: sub_trans sr .
     by apply /setP_P.
  have ->: (induced_order r y) = (induced_order (induced_order r s) y).
    by rewrite iorder_trans.
  apply: total_order_sub =>//; aw.
move=> h.
have p1: sub s (substrate r).
  move=> t ts; set (y:= singleton t).
  have p1: (sub y s) by rewrite/y; apply: set1_sub.
  have p2: (finite_set y) by rewrite /y; apply: set1_finite.
  have p3: (sub y s /\ finite_set y) by split => //.
  move: (h _ p3) => /Zo_P [] /setP_P ysr _.
  apply: ysr; rewrite /y; fprops.
apply: Zo_i; first by apply /setP_P.
move: (iorder_osr or p1) => [pa pb].
split => //; rewrite pb.
move=> x y xs ys; rewrite /ocomparable.
set (z:= doubleton x y).
have p2: (sub z s /\ finite_set z).
  by split; rewrite /z; [ apply: sub_set2 |apply: set2_finite].
move: (h _ p2) => /Zo_P [] /setP_P zsr [oz]; aw => toz.
case: (toz _ _ (set2_1 x y) (set2_2 x y)) => h1; [left | right];
   apply /iorder_gleP => //; exact: (iorder_gle1 h1).
Qed.

Lemma maximal_inclusion s: finite_character s -> nonempty s ->
  exists x, maximal (sub_order s) x.
Proof.
move=>fs nes.
have es: inc emptyset s.
  move: nes=> [x]; rewrite fs=> aux; apply: aux.
  split; [ fprops | apply: emptyset_finite].
set (E:=union s).
  have sp: (sub s (powerset E)) by move=> t ts; apply /setP_P; apply: setU_s1.
apply: (maximal_in_powerset(A:=s) (F:=E)) =>//.
move=> u tou us.
rewrite fs; move=> y [ysu fsy].
case: (emptyset_dichot y) => yne; try ue.
set(Zy:= fun a => choose (fun b=> inc a b /\ inc b u)).
have Zyp: (forall a, inc a y -> (inc a (Zy a) /\ inc (Zy a) u)).
  move=> a ay; rewrite /Zy; apply choose_pr.
  by move: (ysu _ ay)=> aux; move: (setU_hi aux) => [v pa pb]; exists v.
set (Zz:= fun_image y Zy).
have fsZz: (finite_set Zz) by rewrite /Zz; apply: finite_fun_image.
move: (sub_osr Zz) => []; set r:=(sub_order Zz) => pa pb.
have tor: (total_order r).
  split => //; rewrite pb /r /ocomparable;move=> a b aZz bZz.
  have au: (inc a u).
    by move: aZz => /funI_P [z zy ->]; move: (Zyp _ zy)=>[_].
  have bu: (inc b u).
    by move: bZz => /funI_P [z zy ->]; move: (Zyp _ zy)=>[_].
  case: (tou _ _ au bu) =>h; [left | right]; apply /ordo_leP;split => //.
have fsr: (finite_set (substrate r)) by ue.
have ner: nonempty (substrate r).
  move: yne=> [w wy]; exists (Zy w) ; rewrite pb; apply /funI_P; ex_tac.
move: (finite_set_torder_greatest tor fsr ner) => [x [xsr xgr]].
have ysr: (sub y x).
  move => t ty.
  have aux: (inc (Zy t)(substrate r)) by rewrite pb; apply /funI_P; ex_tac.
  move: (xgr _ aux) => /ordo_leP.
  move: (Zyp _ ty)=> [tZ _] [_ _ Zx]; apply: Zx =>//.
rewrite fs; move=> z [zy fsz]; move: (sub_trans zy ysr) => zx.
move: xsr; rewrite pb; move /funI_P=> [w wy Zyw].
move: (Zyp _ wy); rewrite - Zyw; move => [_ xu].
by move: (us _ xu); rewrite fs; apply.
Qed.

Lemma maximal_inclusion_aux: let s := emptyset in
  finite_character s /\
  ~ (exists x, maximal (sub_order s) x ).
Proof.
split.
   move=> x; split; first by move => /in_set0.
   move=> h; have: (inc emptyset emptyset).
     apply: h;split; [ fprops | apply: emptyset_finite].
   by move /in_set0.
by move=> [x [xe _]]; move: xe;rewrite (proj2 (sub_osr _))=> /in_set0.
Qed.

Fixpoint nat_to_B (n:nat) :=
  if n is m.+1 then succ (nat_to_B m) else \0 c.

Lemma nat_to_B_succ n:
  succ (nat_to_B n) = (nat_to_B n.+1).
Proof. by done. Qed.

Lemma nat_to_B_Bnat n: inc (nat_to_B n) Bnat.
Proof.
elim :n; first by simpl; fprops.
by move=> n nB /=; apply: BS_succ.
Qed.

Lemma nat_to_B_injective: injective nat_to_B.
Proof.
elim.
  elim => // n h /= es; move: (@succ_nz (nat_to_B n)); rewrite -es //.
move => n h; elim.
   move=> /= es; move: (@succ_nz (nat_to_B n)); rewrite es //.
move=> m h1 /= aux; congr (_ .+1); apply: h.
move: (CS_Bnat (nat_to_B_Bnat n)) => cn.
move: (CS_Bnat (nat_to_B_Bnat m)) => cm.
exact (succ_injective1 cn cm aux).
Qed.

Lemma nat_to_B_surjective x: inc x Bnat -> exists n, x = nat_to_B n.
Proof.
move: x; apply: cardinal_c_induction.
  by exists 0.
by move=> n nB [m mv]; exists m.+1 ; rewrite mv //.
Qed.

Lemma nat_to_B_sum x y: nat_to_B (x + y) = nat_to_B x +c nat_to_B y.
Proof.
elim: y.
   rewrite addn0 csum0r //; exact (CS_Bnat (nat_to_B_Bnat x)).
move=> n hrec /=; rewrite (csum_via_succ _ (nat_to_B_Bnat n)) addnS - hrec //.
Qed.

Lemma nat_to_B_prod x y: nat_to_B (x * y) = nat_to_B x *c nat_to_B y.
Proof.
elim: y; first by rewrite muln0 cprod0r //.
move=> n hrec /=; rewrite (cprod_via_sum _ (nat_to_B_Bnat n)).
by rewrite mulnS nat_to_B_sum hrec csumC.
Qed.

Lemma nat_to_B_pow x y: nat_to_B (x ^ y) = nat_to_B x ^c nat_to_B y.
Proof.
elim: y; first by rewrite cpowx0 //=; exact succ_zero.
move=> n hrec /=; rewrite (pow_succ _ (nat_to_B_Bnat n)).
by rewrite expnS nat_to_B_prod hrec cprodC.
Qed.

Lemma nat_to_B_le x y: x <=y <-> nat_to_B x <=c nat_to_B y.
Proof.
split.
  move /subnKC => h; move: (nat_to_B_sum x (y - x)); rewrite h => ->.
  apply: csum_M0le; apply: CS_Bnat; apply: nat_to_B_Bnat.
move=> /cardinal_setC1.
set z := (nat_to_B y -c nat_to_B x).
have zb: inc z Bnat by apply: BS_diff; apply: nat_to_B_Bnat.
move: (nat_to_B_surjective zb) => [u uv].
rewrite uv - nat_to_B_sum => h1; move: (nat_to_B_injective h1) => <-.
apply: leq_addr.
Qed.

Lemma nat_to_B_diff x y: nat_to_B (x - y) = nat_to_B x -c nat_to_B y.
Proof.
case: (ltnP x y) => p1.
  move: (ltnW p1) => p2.
  have -> /= : x -y = 0 by apply /eqP.
  rewrite /card_diff.
  by move / nat_to_B_le : p2 => [_ _ /setC_T ->]; rewrite cardinal_set0.
move /nat_to_B_le /cardinal_setC1: (p1).
set u := (nat_to_B x -c nat_to_B y).
have ub: inc u Bnat by apply: BS_diff; apply: nat_to_B_Bnat.
move: (nat_to_B_surjective ub) => [z uv].
by rewrite uv - nat_to_B_sum => /nat_to_B_injective <-; rewrite addKn.
Qed.

Canonical ordering of pairs of ordinals

Definition ordinal_pair x :=
  [/\ pairp x, ordinalp (P x) & ordinalp (Q x)].
Definition ord_pair_le x y:=
   [/\ ordinal_pair x, ordinal_pair y &
   ((P x ) \cup (Q x ) <o (P y ) \cup (Q y )
    \/ ((P x ) \cup (Q x ) = (P y ) \cup (Q y )
        /\ ((P x ) <o (P y )
           \/ (P x = P y /\ Q x <=o Q y ))))].

Lemma ordering_pair1 x: ordinal_pair x ->
   ((P x <=o Q x ) /\ ((P x ) \cup (Q x ) = Q x ))
   \/ ((Q x <=o P x ) /\ ((P x ) \cup (Q x ) = P x )).
Proof.
move=> [px op oq]; case:(ord_le_to_ee op oq)=> h ; [left | right ]; split => //.
  move: h => [_ _ ss]; by apply /setU2id_Pl.
move: h => [_ _ ss]; by apply /setU2id_Pr.
Qed.

Lemma ordering_pair2 x: ordinal_pair x -> ordinalp ((P x ) \cup (Q x )).
Proof.
move=> h; case: (ordering_pair1 h); move => [pa pb]; rewrite pb; ord_tac.
Qed.

Lemma ordering_pair3 x y : ord_pair_le x y ->
  inc x (coarse (succ_o (((P y ) \cup (Q y ))))).
Proof.
move=> [px py le]; apply /setX_P.
move: (ordering_pair2 py) => oo; move: (OS_succ oo) => soo.
suff: inc (P x) (succ_o (P y \cup Q y)) /\ inc (Q x) (succ_o (P y \cup Q y)).
  by move => [pa pb]; split => //;move:px => [ok _].
case: le; move => [le aux].
  case: (ordering_pair1 px); move => [pa pb]; rewrite pb in le;
    split;apply /(ord_ltP soo); apply /ord_lt_succP => //;ord_tac.
case: (ordering_pair1 px); move=> [pa pb];
  split;apply /(ord_ltP soo); apply /ord_lt_succP => //;
    rewrite -le pb => //;apply:ord_leR; ord_tac.
Qed.

Lemma ordering_pair4 x: ordinal_pair x -> ord_pair_le x x.
Proof.
move => op; red; split => //; right; split => //; right; split => //.
by move:op => [_ _ ok]; apply: ord_leR.
Qed.

Lemma well_ordering_pair: worder_r ord_pair_le.
Proof.
move: ordering_pair4 => or1.
have oR: reflexive_rr ord_pair_le.
  by move => x y [p1 p2 _]; split; apply: or1.
have oA: antisymmetric_r ord_pair_le.
  move => x y [p1 p2 p3] [_ _ q3]; case: p3 => p3; case: q3 => q3.
  by move: q3 => [q3 _]; ord_tac.
  by move: q3 => [q3 _]; rewrite q3 in p3; move: p3 => [_].
  by move: p3 => [p3 _]; rewrite p3 in q3; move: q3 => [_].
  move: p3 => [p31 p32]; move: q3 => [q31 q32].
  case: p32 => p32; case: q32 => q32.
    by move: q32 => [q32 _]; ord_tac.
    by move: q32 => [q32 _]; rewrite q32 in p32; move: p32 => [_].
    by move: p32 => [p32 _]; rewrite p32 in q32; move: q32 => [_].
    move: p32 => [pa pb]; move: q32 => [_ pc].
    move: p1 p2 => [px _ _][py _ _]; apply: pair_exten => //; ord_tac.
split.
  split => //.
  move => a b c [p1 p2 p3] [q1 q2 q3].
  split ; [exact | exact | ].
  case: p3 => p3; case: q3 => q3.
  - by left; ord_tac.
  - move: q3 => [q3a q3b];case: q3b => q3b; first by rewrite q3a in p3; left.
     move: q3b => [q4 q5]; left;ue.
  - by move: p3 => [p31 p32]; rewrite -p31 in q3; left.
  - move: p3 q3 => [p3 p4] [q3 q4]; right; split => //; first by ue.
    case:p4=> p4.
      left; case: q4; move => [q4 q5]; [ ord_tac |ue ].
    move: p4 => [ -> p4].
    case: q4; [by left| move=> [p5 p6];right;split => //; ord_tac].
move => x cx [x0 x0x].
set S1:= fun_image x (fun z => (P z ) \cup (Q z )).
have os1: ordinal_set S1.
   move=> t /funI_P [z zx ->].
  move:(cx _ zx) => [pz _ _]; case: (ordering_pair1 pz);
     move=> [pa pb]; rewrite pb; ord_tac.
have nes1: nonempty S1 by exists ((P x0) \cup (Q x0)); apply /funI_P; ex_tac.
move: (ordinal_setI nes1 os1); set gamma:= intersection S1 => gs1.
have g1: forall z, inc z x -> gamma <=o ((P z ) \cup (Q z )).
  move => z zx.
  have aa: inc ((P z) \cup (Q z)) S1 by apply /funI_P; ex_tac.
  move: (os1 _ aa) => ou; split => //.
     by apply os1.
  by apply: setI_s1.
move: gs1 => /funI_P [g0 g0x g0v].
set S2:= fun_image (Zo x (fun z => (P z ) \cup (Q z ) = gamma)) P.
have nes2: nonempty S2.
   by apply: funI_setne; exists g0 => //; apply: Zo_i.
have os2: ordinal_set S2.
  move =>t /funI_P [z /Zo_S zx].
  by move: (cx _ zx) => [[ _ aa _] _ _] ->.
move: (ordinal_setI nes2 os2); set alpha:= intersection S2 => as1.
have a1: forall z, inc z x ->(gamma <o ((P z ) \cup (Q z ))
     \/ (gamma = ((P z ) \cup (Q z )) /\ alpha <=o P z )).
  move=> z zx; move: (g1 _ zx) => le1.
  case: (equal_or_not gamma ((P z) \cup (Q z))) => eq; last by left.
  have pa: inc (P z) S2 by apply/funI_P; exists z => //; apply: Zo_i => //.
  by right;split => //; red; split; fprops;apply: setI_s1.
move: as1 => /funI_P [a0 /Zo_P [a0x ba] qa].
set S3 := fun_image
   (Zo x (fun z => (P z ) \cup (Q z ) = gamma /\ (P z ) = alpha)) Q.
have neS3: nonempty S3.
  by apply: funI_setne; exists a0 => //; apply: Zo_i.
have os3: ordinal_set S3.
  move =>t /funI_P [z /Zo_P [pa _] ->].
  by move: (cx _ pa) => [[_ qb qc] _].
move: (ordinal_setI neS3 os3); set beta:= intersection S3 => as2.
move: as2 => /funI_P [b0 /Zo_P [b0x [pd pb]] pc].
exists b0; red.
rewrite (graph_on_sr cx); split => //.
move=> t tx; apply /graph_on_P1;split => //;split => //.
  by move: (cx _ b0x) => [ok _].
  by move: (cx _ tx) => [ok _].
case: (a1 _ tx); first by rewrite pd => h; left.
rewrite pd; move=> [pe pf]; right; split => //.
rewrite pb; case: (equal_or_not alpha (P t)) => eq1; last by left.
right; split => //; red; split => //.
  by move: (cx _ b0x) => [[_ _ ra] _].
  by move: (cx _ tx) => [[_ _ ra] _].
have pg: inc (Q t) S3 by apply/funI_P; exists t => //; apply: Zo_i => //.
rewrite - pc; apply (setI_s1 pg).
Qed.

Lemma infinite_product_aux k: infinite_c k ->
  (forall z, infinite_c z -> z <o k -> z *c z = z) ->
  let lo:= graph_on ord_pair_le (product k k) in
    k *c k = k /\
  exists2 f, bijection_prop f (product k k) k &
     (forall x y, inc x (source f) -> inc y (source f) ->
       (glt lo x y <-> (Vf f x ) <o (Vf f y ))).
Proof.
move => ik hrec lo.
move: (ik) => [[ok _] _]; move: (ik) => [ck _].
have pa: (forall a, inc a (product k k) -> ord_pair_le a a).
   move => a /setX_P [pa p1a p2a]; apply: ordering_pair4; red;split => //.
     apply: (ordinal_hi ok p1a).
   apply: (ordinal_hi ok p2a).
move: (wordering_pr well_ordering_pair pa); rewrite -/lo; move=> [los low].
move: (OS_ordinal los) (ordinal_o_is los)=> ot [f oisf].
move: (oisf) => [or1 or2 [bf sf tf] isf].
rewrite (ordinal_o_sr (ordinal lo)) in tf.
move: (bf) => [injf [ff sjf]].
have fp1: forall a, inc a (source f) -> ordinalp (Vf f a).
   move => a asf; move: (Vf_target ff asf); rewrite tf.
   apply: (ordinal_hi ot).
have oifp: forall x y, inc x (source f) -> inc y (source f) ->
  (glt lo x y <-> (Vf f x ) <o (Vf f y )).
   move => a b asf bsf; apply:(iff_trans (order_isomorphism_siso oisf asf bsf)).
   split.
     move => [] /ordo_leP [_ _ qa] pb; split => //;split;fprops.
   move => [[_ _ qd] qa]; split => //.
   by apply/ordo_leP;split => //;rewrite - tf; apply: (Vf_target ff).
have otf: ordinalp (target f) by ue.
have pb: forall t, inc t (source f) ->
  cardinal (Vf f t) = cardinal (Zo (source f) (fun z => (glt lo z t))).
  move => t tsf; apply /card_eqP; eqsym.
  set A := (Zo (source f) ((glt lo)^~ t)).
  have As: sub A (source f) by apply Zo_S.
  move: (Vf_target ff tsf) => wt.
  have ra: restriction2_axioms f A (Vf f t).
    red;split => //; [by apply (ordinal_transitive otf wt) | move => w ].
    move => /(Vf_image_P ff As) [u /Zo_P [usf lt] ->].
    by move: lt; rewrite (oifp _ _ usf tsf); move /ord_ltP0 =>[_ _].
  move: (restriction2_fi injf ra).
  set g := restriction2 f A (Vf f t) => injg.
  have sg: source g = A by rewrite /g/restriction2; aw.
  have tg: target g = Vf f t by rewrite /g/restriction2; aw.
  exists g; split => //; split => //; split; first by fct_tac.
  rewrite sg tg; move=> y ytg.
  move: (ordinal_transitive otf wt ytg) => ytf.
  move: (sjf _ ytf) => [w wsf wv]; move: (fp1 _ tsf) => ow.
  have wa: inc w A.
    by apply: Zo_i => //; rewrite (oifp _ _ wsf tsf) wv; apply /ord_ltP.
  exists w => //; rewrite restriction2_V //.
have pc: forall t, inc t (source f) -> cardinal (Vf f t) <c k.
  move => t tsf; rewrite (pb _ tsf).
  set S := (Zo (source f) ((glt lo)^~ t)).
  have qa: sub S (coarse (succ_o (((P t) \cup (Q t))))).
   move => v /Zo_P [vs [/graph_on_P1 [_ _ le] _]]; exact (ordering_pair3 le).
  move: (sub_smaller qa).
  move: tsf; rewrite sf low => tsf1.
  set a := (succ_o ((P t) \cup (Q t))).
  have ->: cardinal (coarse a) = (cardinal a) *c (cardinal a).
    by rewrite /coarse - cprod2_pr1; apply cprod2_pr2; rewrite double_cardinal.
  move=> le1; apply: (card_le_ltT le1).
  case: (finite_dichot (CS_cardinal a)) => fca.
     apply: finite_lt_infinite => //.
     by apply /BnatP; apply: BS_prod; fprops.
  have ak : a <o k.
     apply /ord_ltP => //.
     move: (infinite_card_limit2 ik) => [_ _]; apply.
     move: (tsf1) => /setX_P [_ i1 i2].
      by case: (ordering_pair1 (proj31 (pa _ tsf1))); move => [cd ->].
  move: ak (ak) => [[oa _ _] _].
  move/ (ordinal_cardinal_le2P ck oa) => cak.
  move: (ordinal_cardinal_lt cak) => lt1.
  by rewrite (hrec _ fca lt1).
have pd: sub (ordinal lo) k.
  move => t; rewrite - tf => ttf; move: (sjf _ ttf) => [v vsf <-].
  apply/(ord_ltP ok) /(ordinal_cardinal_le2P ck (fp1 _ vsf)).
  exact: (pc _ vsf).
have pe: k *c k = cardinal (target f).
   rewrite cprod2_pr1; apply /card_eqP; exists f; split => //; ue.
have okok: ordinal lo = k.
  ex_middle xx.
  have : target f <o k by split => //; rewrite tf => //.
  move /(ordinal_cardinal_le2P ck otf).
  move: (cprod_M1le ck (infinite_nz ik)).
  rewrite pe; move => l1 l2; co_tac.
rewrite tf okok (card_card ck) in pe.
split => //;exists f => //; split => //; ue.
Qed.

Lemma infinite_product_alt x : infinite_c x -> x *c x = x.
Proof.
move => ic; ex_middle bad.
pose p z:= infinite_c z /\ z *c z <> z.
have px: p x by split.
have ox: ordinalp x by move: ic => [[ox _] _].
move: (least_ordinal4 ox px); set k := least_ordinal p x.
move=> [ok [ik nkk kl]]; case: nkk.
have kl0: forall z, infinite_c z -> z <o k -> z *c z = z.
   move => z icz zk; ex_middle neq.
   move: (kl _ (proj1 (proj1 icz)) (conj icz neq)) => aux; ord_tac.
by move: (infinite_product_aux ik kl0) => [ xx _ ].
Qed.

Lemma infinite_product_prop2 k: infinite_c k ->
  let lo:= graph_on ord_pair_le (product k k) in
  exists2 f, bijection_prop f (product k k) k &
     (forall x y, inc x (source f) -> inc y (source f) ->
       (glt lo x y <-> (Vf f x ) <o (Vf f y ))).
Proof.
move => ik.
have pa: (forall z, infinite_c z -> z <o k -> z *c z = z).
  by move =>z iz _ ; apply: infinite_product_alt.
by move: (infinite_product_aux ik pa) => [ _ ].
Qed.

End FiniteSets.
Export FiniteSets.