Library sset9

Theory of Sets EIII-5 Properties of integers

Copyright INRIA (2009-2013) Apics; Marelle Team (Jose Grimm).

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

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

Ltac cotac1 := match goal with
    | Ha: inc ?b Bnat, Hb: ?a <c (succ ?b) |- ?a <=c ?b
     => by apply /(card_lt_succ_leP Ha)
    | Ha: inc ?b Bnat, Hb: ?a <=c ?b |- ?a <c (succ ?b)
     => by apply /(card_lt_succ_leP Ha)
    | Ha: inc ?a Bnat, Hb: succ ?a <=c ?b |- ?a <c ?b
     => by apply /(card_le_succ_ltP _ Ha)
    | Ha: inc ?a Bnat, Hb: ?a <c ?b |- succ ?a <=c ?b
     => by apply /(card_le_succ_ltP _ Ha)
end.

Module IntegerProps.

EIII-5-1 Operations on integers and finite sets

Functions on nat

Lemma Bsum_M0le a b: inc a Bnat -> inc b Bnat->
  a <=c (a +c b).
Proof. move=> ca cb; apply: csum_M0le; fprops. Qed.

Lemma Bprod_M1le a b: inc a Bnat -> inc b Bnat->
   b <> \0c -> a <=c (a *c b).
Proof. move=> ca cb; apply: cprod_M1le; fprops. Qed.

Lemma Bnat_to_ell a b: inc a Bnat -> inc b Bnat ->
  [\/ a = b, a <c b | b<c a].
Proof. move=> aB bB; apply: card_le_to_ell; fprops. Qed.

Lemma Bnat_to_el a b: inc a Bnat -> inc b Bnat ->
  a <=c b \/ b <c a.
Proof. move=> aB bB; apply: card_le_to_el; fprops. Qed.

Lemma Bnat_to_ee a b: inc a Bnat -> inc b Bnat ->
  a <=c b \/ b <=c a.
Proof. move=> aB bB; apply: card_le_to_ee; fprops. Qed.

Lemma csum_trivial4 f a:
  card_sum (restr f (singleton a)) = cardinal (Vg f a).
Proof.
have <-: Vg (restr f (singleton a)) a = Vg f a by bw; fprops.
apply: csum_trivial2; rewrite restr_d //.
Qed.

Lemma cprod_trivial4 f a:
  card_prod (restr f (singleton a)) = cardinal (Vg f a).
Proof.
have <-: Vg (restr f (singleton a)) a = Vg f a by bw ; fprops.
apply: cprod_trivial2; rewrite restr_d //.
Qed.

Lemma csum_increasing6 f j: cardinal_fam f ->
  inc j (domain f) -> (Vg f j) <=c (card_sum f).
Proof.
move=> cf jd.
move: (csum_increasing1 cf (set1_sub jd)).
by rewrite csum_trivial4 (card_card (cf _ jd)).
Qed.

Lemma cprod_increasing6 f j: cardinal_fam f -> card_nz_fam f ->
  inc j (domain f) -> (Vg f j) <=c (card_prod f).
Proof.
move=> cf alnz jd.
move: (cprod_increasing1 cf alnz (set1_sub jd)).
by rewrite cprod_trivial4 (card_card (cf _ jd)).
Qed.

Lemma induction_sum0 f a b: (~ inc b a) ->
  card_sum (restr f (a +s1 b)) =
  card_sum (restr f a) +c (Vg f b).
Proof. move => nba; exact: (csumA_setU1 (Vg f) nba). Qed.

Lemma induction_prod0 f a b: (~ inc b a) ->
  card_prod (restr f (a +s1 b)) =
  (card_prod (restr f a)) *c (Vg f b) .
Proof. move => nba; exact: (cprodA_setU1 (Vg f) nba). Qed.

Lemma induction_sum1 f a b:
  domain f = a +s1 b -> (~ inc b a) ->
  card_sum f = card_sum (restr f a) +c (Vg f b).
Proof.
by move=> df nba; rewrite - (induction_sum0 _ nba) -df card_sum_gr.
Qed.

Lemma induction_prod1 f a b:
  domain f = a +s1 b -> (~ inc b a) ->
  card_prod f = card_prod (restr f a) *c (Vg f b).
Proof.
by move=> df nba; rewrite - (induction_prod0 _ nba) - df - card_prod_gr.
Qed.

Definition of a finite family of integers

Definition finite_int_fam f:=
  (allf f (inc ^~Bnat)) /\ finite_set (domain f).

A finite sum or product of integers is an integer

Section FiniteIntFam.
Variable f: Set.
Hypothesis fif: finite_int_fam f.

Lemma finite_sum_finite_aux x:
  sub x (domain f) -> inc (card_sum (restr f x)) Bnat.
Proof.
move: fif => [alB fsd] sxd.
move: (sub_finite_set sxd fsd) => fsx.
move: x fsx sxd.
apply: finite_set_induction0.
  move=> _;rewrite csum_trivial; fprops; bw; fprops.
move=> a b ap nba st.
move: (alB _ (st _ (setU1_1 b a))) => vb.
rewrite induction_sum0 =>//.
apply: BS_sum =>//; apply: ap; apply: sub_trans st; fprops.
Qed.

Lemma finite_product_finite_aux x:
  sub x (domain f) -> inc (card_prod (restr f x)) Bnat.
Proof.
move: fif => [alB fsd] sxd.
have fsx:=(sub_finite_set sxd fsd).
move: x fsx sxd.
apply: finite_set_induction0.
  rewrite cprod_trivial;fprops; bw; fprops.
move=> a b ap nba st.
rewrite induction_prod0 =>//.
have ha:= (@sub_setU1 b a) ; have hb:= (setU1_1 b a).
exact: (BS_prod (ap (sub_trans ha st)) (alB _ (st _ hb))).
Qed.

Theorem finite_sum_finite: inc (card_sum f) Bnat.
Proof.
rewrite - card_sum_gr;apply: finite_sum_finite_aux;fprops.
Qed.

Theorem finite_product_finite: inc (card_prod f) Bnat.
Proof.
rewrite - card_prod_gr; apply: finite_product_finite_aux; fprops.
Qed.

End FiniteIntFam.

Finite unions and products of finite sets are finite sets

Lemma finite_union_finite f:
  (allf f finite_set) -> finite_set (domain f) -> finite_set (unionb f).
Proof.
move=> alf fsd.
set (g:= Lg (domain f) (fun a => cardinal (Vg f a))).
have dg: (domain g = domain f) by rewrite /g; bw.
have fif: (finite_int_fam g).
  split => //; last by ue.
    rewrite /g;fprops.
  by red; rewrite dg /g; move=> i idf; bw;apply /BnatP; apply: alf.
move: (csum_pr1 f) (finite_sum_finite fif) ; rewrite -/g => f2 xB.
by apply/card_finite_setP; apply: (BS_le_int f2).
Qed.

Lemma finite_product_finite_set f: (allf f finite_set)
  -> finite_set (domain f) -> finite_set(productb f).
Proof.
move=> alf fsd.
set (g:= Lg (domain f) (fun a => cardinal (Vg f a))).
have dg: (domain g = domain f) by rewrite /g;bw.
red;rewrite cprod_pr//; apply: Bnat_hi.
apply: finite_product_finite; split => //;last by ue.
by red; bw; move=> i idf; bw; apply /BnatP;apply: alf.
Qed.

EIII-5-2 Strict inequalities between integers

If a<b there is a strictly positive c such that c=a*b

Lemma strict_pos_P1 a: inc a Bnat ->
  (a <> \0c <-> \0c <c a).
Proof.
move => aB; split => h; first by apply : card_ne0_pos; fprops.
by move: h => [_ /nesym].
Qed.

Lemma strict_pos_P a: inc a Bnat ->
  (\0c <> a <-> \0c <c a).
Proof.
by move => aB; apply:(iff_trans _ (strict_pos_P1 aB)); split; apply nesym.
Qed.

Theorem card_ltP a b: inc a Bnat -> inc b Bnat ->
  (a <c b <-> exists c, [/\ inc c Bnat, c <> \0c & a +c c = b]).
Proof.
move=> aB bB; split.
  move=> [ab nab]; move: (BS_diff a bB) => pa; ex_tac.
    by apply: cdiff_nz.
  by rewrite (cardinal_setC1 ab).
move=> [c [cB cnz <-]].
move: (card_lt_succ aB); rewrite (Bsucc_rw aB) => asa.
have p2: (a +c \1c) <=c (a +c c).
   apply: csum_Mlele; fprops; apply: card_ge1; fprops.
co_tac.
Qed.

Compatibility of sum and product with strict order

Lemma csum_Mlelt a b a' b':
  inc a' Bnat -> inc b' Bnat->
  a <=c a' -> b <c b' -> (a +c b) <c (a' +c b').
Proof.
move=> a'B b'B aa' bb'.
have bB: inc b Bnat by Bnat_tac.
move/ (card_ltP bB b'B):bb' => [c [cB cnz <-]].
apply: (@card_le_ltT _ (a' +c b)).
   apply: csum_Mlele; fprops.
by rewrite csumA; apply card_ltP;fprops; exists c.
Qed.

Lemma csum_Mlteq a a' b:
  inc b Bnat -> inc a' Bnat ->
  a <c a' -> (a +c b) <c (a'+c b).
Proof.
move=> bB a'B aa'; rewrite csumC (csumC a' b); apply: csum_Mlelt; fprops.
Qed.

Lemma csum_Meqlt a a' b:
  inc b Bnat -> inc a' Bnat ->
  a <c a' -> (b +c a) <c (b +c a').
Proof.
by rewrite (csumC b) (csumC b); exact:csum_Mlteq.
Qed.

Lemma csum_M0lt a b: inc a Bnat -> inc b Bnat -> \0c <c b -> a <c a +c b.
Proof.
move => aB bB bp.
rewrite -{1} (csum0r (CS_Bnat aB)); apply:csum_Meqlt => //.
Qed.
Lemma finite_sum4_lt a b: inc b Bnat ->
   a <> \0c -> b <c (b +c a).
Proof.
move=> bB anz.
rewrite - csum2_pr2b.
have az: \0c <c cardinal a.
  split; first by apply: czero_least; fprops.
  by apply: nesym;apply:cardinal_nonemptyset0.
rewrite csumC.
move: (CS_Bnat bB) => cb.
case: (finite_dichot (CS_cardinal a)).
  move /BnatP => aB; move: (csum_Mlteq bB aB az); aw.
move => ia.
apply: card_lt_leT (csum_M0le b (proj1 ia)).
apply: finite_lt_infinite; fprops.
Qed.

Lemma cprod_Mlelt a b a' b':
  inc a' Bnat -> inc b' Bnat->
  a <=c a' -> b <c b' -> a' <> \0c ->
  (a *c b) <c (a' *c b').
Proof.
move=> a'B b'B aa' bb'.
have bB: inc b Bnat by Bnat_tac.
move /(card_ltP bB b'B):bb' => [c [cB cnz <-]] anz.
apply: (@card_le_ltT _ (a' *c b)).
  apply: cprod_Mlele; fprops.
move: (BS_prod a'B cB) => pB.
rewrite cprod_sumDl; apply /card_ltP; fprops;ex_tac.
by apply: cprod2_nz.
Qed.

Theorem finite_sum_lt f g:
  finite_int_fam f -> finite_int_fam g -> domain f = domain g ->
  (forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)) ->
  (exists2 i, inc i (domain f) & (Vg f i) <c (Vg g i)) ->
  (card_sum f) <c (card_sum g).
Proof.
move=> fif fig df ale [i ifg lti].
move: (fif)(fig)=> [f2 f3] [g2 g3].
have idg: inc i (domain g) by rewrite -df.
move: (setC1_K ifg) => dtc; symmetry in dtc.
have incd: ~ (inc i (complement (domain f) (singleton i))).
  by move=> /setC1_P [_ ]; aw => aux; case: aux.
have sd: sub ((domain f) -s1 i) (domain f) by apply: sub_setC.
have sdg: sub ((domain g) -s1 i) (domain g) by apply: sub_setC.
rewrite (induction_sum1 dtc incd).
rewrite df in dtc incd; rewrite (induction_sum1 dtc incd).
have afB: inc (Vg f i) Bnat by apply: f2.
have agB: inc (Vg g i) Bnat by apply: g2.
apply: csum_Mlelt =>//.
  apply: finite_sum_finite_aux=>//.
apply: csum_increasing;fprops; bw; first by ue.
move=> x xd; bw; rewrite - ?df;fprops.
Qed.

Theorem finite_product_lt f g:
  finite_int_fam f -> finite_int_fam g -> domain f = domain g ->
  (forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)) ->
  (exists2 i, inc i (domain f) & (Vg f i) <c (Vg g i)) ->
  card_nz_fam g ->
  (card_prod f) <c (card_prod g).
Proof.
move=> fif fig df ale [i ifg lti] alne.
move: (fif)(fig)=> [f2 f3] [g2 g3].
have idg: inc i (domain g) by rewrite -df.
have afB: inc (Vg f i) Bnat by apply: f2.
have agB: inc (Vg g i) Bnat by apply: g2.
have sd: sub ((domain f) -s1 i) (domain f) by apply: sub_setC.
have sdg: sub ((domain g) -s1 i) (domain g) by apply: sub_setC.
have incd: ~ (inc i ((domain f) -s1 i)).
  by move=> /setC1_P [_ ]; aw => aux; case: aux.
move: (setC1_K ifg) => dtc; symmetry in dtc.
rewrite (induction_prod1 dtc incd).
rewrite df in dtc incd; rewrite (induction_prod1 dtc incd).
apply: cprod_Mlelt =>//.
      apply: finite_product_finite_aux=>//.
  apply: cprod_increasing;fprops; bw; first by ue.
  move=> x xd; bw=>//; rewrite - ?df;fprops.
apply/cprod_nzP; fprops.
red;rewrite restr_d; fprops.
move=> j jdg; move: (jdg) => /setC1_P [jd _]; bw;apply: (alne _ jd).
Qed.

Lemma cprod_M1lt a b: inc a Bnat -> inc b Bnat ->
  a <> \0c -> \1c <c b -> a <c (a *c b).
Proof.
move=> aB bB naz c1b.
move: (CS_Bnat aB) => ca.
move: (cprod_Mlelt aB bB (card_leR ca) c1b naz).
by rewrite cprod1r.
Qed.

Compatibility of power and order

Lemma cpow_nz a b: a<> \0c -> (a ^c b) <> \0c.
Proof.
move=> anz;rewrite - cpow_pr2; apply /cprod_nzP ; red; bw => t tb; bw.
Qed.

Lemma cpow2_nz x: \2c ^c x <> \0c.
Proof. apply: cpow_nz; fprops. Qed.

Lemma cpow_Mltle a a' b:
  inc a' Bnat -> inc b Bnat->
  a <c a' -> b <> \0c -> (a ^c b) <c (a' ^c b).
Proof.
move=> a'B bB aa' nzb.
move: (cpred_pr bB nzb) => [pB bs].
have nza': a'<> \0c.
  by move => h; rewrite h in aa'; apply: (card_lt0 aa').
case: (equal_or_not a \0c).
  move=> ->; rewrite cpow0x //; split.
    move: (BS_pow a'B bB) => poB; apply: czero_least; fprops.
  apply: nesym; apply: cpow_nz;fprops.
move => nz.
rewrite bs (pow_succ a pB)(pow_succ a' pB).
have p1: a <=c a' by move: aa' => [ok _].
have p2: (cpred b) <=c (cpred b) by fprops.
move: (BS_pow a'B pB) => ca'.
move: (cpow_Mlele nz p1 p2) => p3.
apply: (cprod_Mlelt ca' a'B p3 aa').
apply: cpow_nz;fprops.
Qed.

Lemma cpow_Mlelt a b b':
  inc a Bnat -> inc b' Bnat->
  b <c b' -> \1c <c a -> (a ^c b) <c (a ^c b').
Proof.
move=> aB b'B bb' l1a.
have anz: a <> \0c by move: l1a=> [/card_ge1P [_ /nesym h] _].
have bB: inc b Bnat by Bnat_tac.
move: bb' => /(card_ltP bB b'B) [c [cB cnz <-]].
have ca:cardinalp a by fprops.
move:(cpow_Mle1 ca cnz) => le1.
rewrite cpow_sum2; apply: cprod_M1lt; fprops.
  apply: cpow_nz; fprops.
co_tac.
Qed.

Lemma cpow_M1lt a b: cardinalp a -> \1c <c b -> a <c (b ^c a).
Proof.
move => ca [ /card_ge1P [ww /nesym h] bn1].
apply(card_lt_leT (cantor ca)).
apply: cpow_Mlele; fprops;apply: card_ge2; fprops;co_tac.
Qed.

Injectivity of sum and product

Lemma csum_simplifiable_left a b b':
  inc a Bnat -> inc b Bnat -> inc b' Bnat ->
  a +c b = a +c b' -> b = b'.
Proof.
move=> aB bB bB' eql.
have laa: a <=c a by fprops.
case: (Bnat_to_ell bB bB') =>// aux.
  by move: (csum_Mlelt aB bB' laa aux)=> [_ h].
by move: (csum_Mlelt aB bB laa aux)=> [_ []].
Qed.

Lemma csum_simplifiable_right a b b':
  inc a Bnat -> inc b Bnat -> inc b' Bnat ->
  b +c a = b' +c a -> b = b'.
Proof.
move=> aB bB b'B;
rewrite csumC (csumC b' a).
by apply: csum_simplifiable_left.
Qed.

Lemma cprod_simplifiable_left a b b':
  inc a Bnat -> inc b Bnat -> inc b' Bnat ->
  a <> \0c -> a *c b = a *c b' -> b = b'.
Proof.
move=> aB bB bB' naz eql.
have laa: a <=c a by fprops.
case: (Bnat_to_ell bB bB') =>// aux.
  by move: (cprod_Mlelt aB bB' laa aux naz)=> [_ h].
by move: (cprod_Mlelt aB bB laa aux naz)=> [_ []].
Qed.

Lemma cprod_simplifiable_right a b b':
  inc a Bnat -> inc b Bnat -> inc b' Bnat ->
  a <> \0c -> b *c a = b' *c a -> b = b'.
Proof.
by move=> aB bB b'B;rewrite cprodC (cprodC b' a);apply: cprod_simplifiable_left.
Qed.

cardinal difference

Lemma cdiff_wrong a b: a <=c b -> a -c b = \0c.
Proof.
by move => [_ _ ab]; rewrite /card_diff (setC_T ab) cardinal_set0.
Qed.

Lemma cdiff_pr a b:
  b <=c a -> b +c (a -c b) = a.
Proof. apply: cardinal_setC1. Qed.

Lemma cdiff_pr0 a b: inc a Bnat-> inc b Bnat ->
  b <=c a -> (inc (a -c b) Bnat /\ b +c (a -c b) = a).
Proof. move=> aB bB h; split; [ fprops | by apply: cdiff_pr]. Qed.

Lemma cdiff_pr1 a b: inc a Bnat-> inc b Bnat ->
  (a +c b) -c b = a.
Proof.
move=> aB bB.
move: (BS_sum aB bB)=> sB.
move: (Bsum_M0le bB aB); rewrite csumC=> aux.
move: (cdiff_pr aux); rewrite csumC=> aux'.
apply: (csum_simplifiable_right bB (BS_diff _ sB) aB aux').
Qed.

Lemma cdiff_rpr a b:
  b <=c a -> (a -c b) +c b = a.
Proof. by move=> leaB;rewrite csumC; apply: cdiff_pr. Qed.

Lemma cdiff_pr2 a b c: inc a Bnat-> inc b Bnat ->
  a +c b = c -> c -c b = a.
Proof. by move=> aB bB h; move: (cdiff_pr1 aB bB); rewrite h. Qed.

Lemma cdiff_pr3 a b n:
   inc n Bnat -> a <=c b -> b <=c n -> (n -c b) <=c (n -c a).
Proof.
move => mB le1 le2.
have bB:=(BS_le_int le2 mB).
have aB:=(BS_le_int le1 bB).
have dB:=(BS_sum (BS_diff a bB) (BS_diff b mB)).
rewrite - {2} (cdiff_pr le2).
rewrite -{2} (cdiff_pr le1) - csumA (csumC a) (cdiff_pr1 dB aB) csumC.
apply:(csum_M0le _ (CS_diff n b)).
Qed.

Lemma cdiff_pr7 a b c:
  a <=c b -> b <c c -> inc c Bnat -> (b -c a) <c (c -c a).
Proof.
move => le1 lt2 cB.
have bB:= (BS_lt_int lt2 cB).
have aB:= (BS_le_int le1 bB).
move:(BS_diff a bB) (BS_diff b cB) => ha hb.
rewrite -(cdiff_pr (proj1 lt2)) - {2}(cdiff_pr le1) - csumA csumC.
rewrite (cdiff_pr1 (BS_sum ha hb) aB);apply: (csum_M0lt ha hb).
split; [ apply: czero_least;fprops | apply: (nesym (cdiff_nz lt2))].
Qed.

Lemma cardinal_setC4 E A: sub A E ->
  finite_set E -> cardinal (E -s A) = (cardinal E) -c (cardinal A).
Proof.
move => AE fe.
move: (cardinal_setC AE) =>cc.
have ccEA: cardinalp (cardinal (E -s A)) by fprops.
have ccA: cardinalp (cardinal A) by fprops.
symmetry; rewrite - cc csumC.
move: fe => /BnatP; rewrite - cc => sB.
apply: cdiff_pr1 =>//.
   apply: (Bnat_in_sum ccEA sB).
rewrite csumC in sB;apply: (Bnat_in_sum ccA sB).
Qed.

Lemma cdiff_n_n a: a -c a = \0c.
Proof. by rewrite /card_diff setC_v cardinal_set0. Qed.

Lemma cdiff_n_0 a: inc a Bnat -> a -c \0c = a.
Proof. move=> aB; apply: cdiff_pr2; fprops; aw; fprops. Qed.

Lemma cdiff_pr4 a b a' b': inc a Bnat-> inc b Bnat ->
  inc a' Bnat-> inc b' Bnat ->
  a <=c b -> a' <=c b' ->
  (b +c b') -c (a +c a') = (b -c a) +c (b' -c a').
Proof.
move=> aB bB a'B b'B ab a'b'.
apply: cdiff_pr2; [ fprops | fprops |].
have aux: ((b -c a) +c b') +c a = b' +c b.
  by rewrite (csumC _ b') - csumA cdiff_rpr.
by rewrite (csumC a a') csumA - (csumA _ _ a') (cdiff_rpr a'b') aux csumC.
Qed.

Lemma cdiffA a b c:
  inc a Bnat -> inc b Bnat -> inc c Bnat ->
  (b +c c) <=c a -> (a -c b) -c c = a -c (b +c c).
Proof.
move=> aB bB cB h.
move: (cdiff_pr h) => aux.
apply: cdiff_pr2 =>//; first by fprops.
symmetry; apply: cdiff_pr2; fprops.
by rewrite - csumA csumC (csumC c b).
Qed.

Lemma cpred_pr4 a: cardinalp a -> cpred a = a -c \1c.
Proof.
move=> ca.
case: (finite_dichot ca).
  case/finite_succ => anz.
    rewrite /cpred /card_diff anz setU_0 setC_T ?cardinal_set0; fprops.
  move: anz => [y fy sy].
  rewrite sy - {2} (succ_of_finite fy) (card_succ_pr4 (CS_finite_o fy)).
  by rewrite /cpred (succo_K (proj1 fy)) (cdiff_pr1 _ BS1) //; apply /BnatP.
rewrite /cpred /card_diff.
move => pa; move: (proj1 (proj1 pa)) => oa.
move: (infinite_card_limit2 pa)=> pb.
move /(limit_ordinal_P1 oa): pb => [ane <-].
move: (ord_ne_pos oa ane) => /(ord_ltP oa) a0.
move: (ordinal_irreflexive oa) => ia.
rewrite -[a -s \1c] /(a -s1 \0o) -{1} (card_card ca); apply /card_eqP.
have: a +s1 a \Eq ((a -s1 \0o) +s1 \0o).
  rewrite (setC1_K a0); eqsym;move: pa => [] //.
by move /(setU1_injective_card2 ia (@setC1_1 \0o a)).
Qed.

Lemma cdiff_nz1 a b: inc a Bnat -> inc b Bnat ->
  (succ b) <=c a -> a -c b <> \0c.
Proof.
move=> aB bB lesba; apply: cdiff_nz => //; apply /card_le_succ_ltP => //.
Qed.

Lemma cdiff_A1 a b: inc a Bnat -> inc b Bnat ->
  (succ b) <=c a -> cpred (a -c b) = a -c (succ b).
Proof.
move=> aB bB; rewrite (Bsucc_rw bB) => h'.
rewrite - cdiffA; fprops; apply: cpred_pr4; fprops.
Qed.

Lemma cdiff_le_symmetry a b:
  b <=c a -> (a -c b) <=c a.
Proof.
move=> ba; move:(cdiff_pr ba) => aux.
rewrite -{2} aux csumC; apply: csum_M0le; apply:CS_diff.
Qed.

Lemma cdiff_lt_symmetry n p: inc p Bnat ->
  n <c p -> (cpred (p -c n)) <c p.
Proof.
move=> pB ltnp.
have snz := (cdiff_nz ltnp).
move: ltnp => [lenp _].
move: (cdiff_pr0 pB (BS_le_int lenp pB) lenp) => [sf aux].
move: (cpred_pr sf snz)=> [aa bb].
apply /(card_le_succ_ltP _ aa); rewrite - bb; apply: (cdiff_le_symmetry lenp).
Qed.

Lemma double_diff n p: inc n Bnat ->
  p <=c n -> n -c (n -c p) = p.
Proof.
move=> nB lepn.
move: (BS_le_int lepn nB) => pB.
apply: cdiff_pr2; [exact pB | fprops | apply: cdiff_pr=>//].
Qed.

Lemma csucc_diff a b: inc a Bnat -> inc b Bnat ->
  (succ b) <=c a -> a -c b = succ (a -c (succ b)).
Proof.
move=> aB bB aux; move: (BS_succ bB) => sB.
apply: cdiff_pr2 ; fprops.
have sb: inc (a -c (succ b)) Bnat by fprops.
rewrite (Bsucc_rw sb) - csumA.
have->: (\1c +c b = succ b) by rewrite (Bsucc_rw bB) csumC.
apply: cdiff_rpr =>//.
Qed.

Lemma cardinal_complement_image1 f: injection f ->
  (cardinal ((target f) -s (image_of_fun f))) +c (cardinal (source f))
  = cardinal (target f).
Proof.
move => injf.
set A:= (image_of_fun f).
have ->: (cardinal (source f) = cardinal A).
  apply /card_eqP;exists (restriction_to_image f).
  rewrite /restriction_to_image/restriction2; red;aw; split => //.
  by apply: (restriction_to_image_fb injf).
symmetry; rewrite csumC.
set B:= (target f) -s A.
have p0: sub A (target f) by apply: fun_image_Starget; fct_tac.
have <-: A \cup B = target f by apply: setU2_Cr.
rewrite csum2_pr2a csum2_pr2b csum2_pr5 //;apply: set_I2Cr.
Qed.

Lemma cardinal_complement_image f: injection f ->
  finite_set (target f) ->
    cardinal ((target f) -s (image_of_fun f)) =
    (cardinal (target f)) -c (cardinal (source f)).
Proof.
move=> injf fst.
move: (cardinal_complement_image1 injf).
move: fst => /BnatP fb h.
rewrite - h in fb |- *.
have aB := (Bnat_in_sum (CS_cardinal (source f)) fb).
have cB:= (Bnat_in_sum2 (CS_cardinal (target f -s image_of_fun f)) fb).
by symmetry;apply: cdiff_pr1.
Qed.


Lemma Bnat_le_R a: inc a Bnat -> a <=N a.
Proof. move => aB; split;fprops. Qed.

Lemma Bnat_le_T a b c: a <=N b -> b <=N c -> a <=N c.
Proof.
move /Bnat_order_leP => ab /Bnat_order_leP bc; apply /Bnat_order_leP.
move: Bnat_order_wor=> [[or wor] _]; order_tac.
Qed.

Lemma Bnat_le_A a b: a <=N b -> b <=N a -> a = b.
Proof.
move /Bnat_order_leP => ab /Bnat_order_leP ba.
move: Bnat_order_wor=> [[or wor] _]; order_tac.
Qed.

Lemma Bnato_to_el a b: inc a Bnat -> inc b Bnat ->
  a <=N b \/ b <N a.
Proof.
move=> aB bB.
move:Bnat_order_wor=> [wor sr].
move: (worder_total wor)=> [or prop].
case: (equal_or_not b a).
  move=>->; left; apply /Bnat_order_leP.
  order_tac; by rewrite sr.
rewrite sr in prop; case: (prop _ _ aB bB); move /Bnat_order_leP.
  by left.
by move => pa pb; right; split.
Qed.

Lemma csum_le_simplifiable a b c:
  inc a Bnat -> inc b Bnat -> inc c Bnat->
  (a +c b) <=c (a +c c) -> b <=c c.
Proof.
move=> aB bB cB abc.
case: (Bnat_to_el bB cB) => // ltcb.
move: (csum_Mlelt aB bB (card_leR (CS_Bnat aB)) ltcb)=> h; co_tac.
Qed.

Lemma csum_lt_simplifiable a b c:
  inc a Bnat -> inc b Bnat -> inc c Bnat->
  (a +c b) <c (a +c c) -> b <c c.
Proof.
move=> aB bB cB [abc nac]; split.
  apply: (csum_le_simplifiable aB bB cB abc).
by dneg bc; rewrite bc.
Qed.

Lemma cprod_le_simplifiable a b c:
  inc a Bnat -> inc b Bnat -> inc c Bnat-> a <> \0c ->
  (a *c b) <=c (a *c c) -> b <=c c.
Proof.
move=>aB bB cB naz abc.
case: (Bnat_to_el bB cB) => // ltcb.
move: (cprod_Mlelt aB bB (card_leR (CS_Bnat aB)) ltcb naz)=> h; co_tac.
Qed.

Lemma cprod_lt_simplifiable a b c:
  inc a Bnat -> inc b Bnat -> inc c Bnat-> a <> \0c ->
  (a *c b) <c (a *c c) -> b <c c.
Proof.
move=> aB bB cB naz [abc nac]; split.
   by apply: (cprod_le_simplifiable aB).
by dneg bc; rewrite bc.
Qed.

Lemma cdiff_pr5 a b c: inc a Bnat -> inc b Bnat -> inc c Bnat ->
  (a +c c) -c (b +c c) = a -c b.
Proof.
move => aB bB cB.
case: (Bnat_to_ee aB bB) => ab.
  symmetry; rewrite (cdiff_wrong ab) (cdiff_wrong) //.
  by apply:csum_Mleeq.
by apply:cdiff_pr2; fprops; rewrite csumA (csumC _ b) cdiff_pr.
Qed.

Lemma cdiff_pr6 a b: inc a Bnat -> inc b Bnat ->
  (succ a) -c (succ b) = a -c b.
Proof.
move=> aB bB; rewrite !Bsucc_rw //;apply: cdiff_pr5 =>//; fprops.
Qed.

Lemma cdiff_increasing2 a b c: inc a Bnat -> inc b Bnat ->
  c <=c (a +c b) -> (c -c b) <=c a.
Proof.
move=> aB bB cab.
move: (BS_le_int cab (BS_sum aB bB)) => cB.
case: (Bnat_to_ee cB bB) => cb; first by rewrite cdiff_wrong; fprops.
apply: (csum_le_simplifiable (a:= b)); fprops.
rewrite csumC in cab; rewrite cdiff_pr //.
Qed.

Lemma cdiff_increasing3 a b c: inc a Bnat ->inc c Bnat ->
  b <=c c -> c <c (a +c b) -> (c -c b) <c a.
Proof.
move=> aB cB bc cab.
move: (BS_le_int bc cB) => bB.
apply: (csum_lt_simplifiable (a:= b)); fprops.
rewrite csumC in cab; rewrite cdiff_pr //.
Qed.

EIII-5-3 Intervals in sets of integers

Definition Bintcc a b := interval_cc Bnat_order a b.
Definition Bint a:= interval_co Bnat_order \0c a.
Definition Bintc a:= Bintcc \0c a.
Definition Bint1c a:= Bintcc \1c a.

Definition Bint_cco a b :=
  graph_on cardinal_le (interval_cc Bnat_order a b).

Lemma Bintc_i b x: inc x (Bintc b) -> x <=c b.
Proof. by move /Bint_ccP => [_ [_ _ h]]. Qed.

Lemma BintcP b: inc b Bnat -> forall x, (inc x (Bintc b) <-> x <=c b).
Proof.
move=> bB x; split; first by apply: Bintc_i.
move => h;apply /(Bint_ccP1 BS0 bB); split => //; apply: czero_least; co_tac.
Qed.

Lemma Bint1cP b: inc b Bnat -> forall x,
  (inc x (Bint1c b) <-> (x <> \0c /\ x <=c b)).
Proof.
move=> bB x; apply: (iff_trans (Bint_ccP1 BS1 bB x)).
split.
  move => [pa pb];split => //.
  move=> bz; rewrite bz in pa.
  move: (card_le0 pa); apply: card1_nz.
move => [x0 xb]; split => //.
by move: xb => [cb _ _]; apply: card_ge1.
Qed.

Lemma Bint1cPb b: inc b Bnat -> forall x,
  (inc x (Bint1c b) <-> (\1c <=c x /\ x <=c b)).
Proof. move=> aB x; apply: (Bint_ccP1 BS1 aB). Qed.

Lemma Bint_S a b: sub (Bintcc a b) Bnat.
Proof. rewrite /Bintcc /interval_cc (proj2 Bnat_order_wor); apply: Zo_S. Qed.

Lemma Bint_S1 a: sub (Bint a) Bnat.
Proof. rewrite /Bint /interval_co (proj2 Bnat_order_wor); apply: Zo_S. Qed.

Lemma Bint_i a x: inc x (Bint a) -> x <c a.
Proof. by move => /Bint_coP [_ [[_ _ ha] hb]]; split. Qed.

Lemma BintP a: inc a Bnat -> forall x,
  (inc x (Bint a) <-> x <c a).
Proof.
move=> aB x; split; first by apply:Bint_i.
move => xa; apply/(Bint_coP1 BS0 aB); split => //.
apply: czero_least; co_tac.
Qed.

Lemma BintsP a: inc a Bnat -> forall x,
  (inc x (Bint (succ a)) <-> x <=c a).
Proof.
move=> aB x; apply: (iff_trans (Bint_coP1 BS0 (BS_succ aB) x)); split.
  by move => [_ [pa pb]]; apply /(card_lt_succ_leP aB); split.
move => lxa;split; first by apply: czero_least; co_tac.
by apply /(card_lt_succ_leP aB).
Qed.

Lemma Bint_co_cc p: inc p Bnat -> Bintc p = Bint (succ p).
Proof.
move => pB; set_extens x.
  by move/(BintcP pB) /(BintsP pB).
by move /(BintsP pB)/(BintcP pB).
Qed.

Lemma Bint_co00: Bint \0c = emptyset.
Proof. apply /set0_P=> t; move /(BintP BS0); apply: card_lt0. Qed.

Lemma Bint_co01: (inc \0o (Bint \1c) /\ Bint \1c = singleton \0c).
Proof.
have zi: inc \0c (Bint \1c).
   apply/(BintP BS1); apply: card_lt_01.
split => //.
apply: set1_pr => // z /(BintP BS1).
rewrite - succ_zero; move/(card_lt_succ_leP BS0);apply: card_le0.
Qed.

Lemma Bint_cc00: Bintc \0c = singleton \0c.
Proof.
by rewrite -(proj2 Bint_co01) - succ_zero (Bint_co_cc BS0).
Qed.

Lemma Bintc_M a b: inc b Bnat ->
  a <=c b -> sub (Bintc a) (Bintc b).
Proof. move=> bB ab t /(Bintc_i) ta; apply /(BintcP bB); co_tac. Qed.

Lemma Bintc_M1 a: inc a Bnat ->
  sub (Bintc a) (Bintc (succ a)).
Proof. move=> aB;apply: Bintc_M; fprops. Qed.

Lemma Bint_si a: inc a Bnat ->
  inc a (Bint (succ a)).
Proof. move=> aB; apply /(BintsP aB); fprops. Qed.

Lemma Bint_M a: inc a Bnat -> sub (Bint a) (Bint (succ a)).
Proof.
move=> aB t /(BintP aB) tx; apply/(BintsP aB); co_tac.
Qed.

Lemma Bint_M1 a b: inc b Bnat -> a <=c b -> sub (Bint a) (Bint b).
Proof.
move=> bB ab r /Bint_i ra; apply /(BintP bB); co_tac.
Qed.

Lemma Bint_pr4 n: inc n Bnat ->
  ( ((Bint n) +s1 n = (Bint (succ n)))
    /\ ~(inc n (Bint n))).
Proof.
move=> nB.
split; last by move/(BintP nB) => [_].
set_extens t.
   case/setU1_P.
    by apply:Bint_M.
    by move => ->; apply:Bint_si.
move /(BintsP nB) => tn; apply/setU1_P.
case: (equal_or_not t n); first by right.
by move => ntn; left; apply/(BintP nB); split.
Qed.

Lemma Bint_pr5 n (si := Bintcc \1c n): inc n Bnat ->
  ( (si +s1 \0c = Bintc n) /\ ~(inc \0c si)).
Proof.
move=> nB; split.
  set_extens x.
    case /setU1_P; first by move /(Bint_ccP1 BS1 nB) => [_]/(BintcP nB).
    move => ->; apply /(BintcP nB); fprops.
  move /(BintcP nB) => h; apply /setU1_P.
  case: (equal_or_not x \0c) => xz; [right => //| left => // ].
  apply /(Bint_ccP1 BS1 nB);split => //;apply: card_ge1 => //;co_tac.
move /(Bint_ccP1 BS1 nB) => [h _].
move: card_lt_01 => xx; co_tac.
Qed.

Lemma incsx_intsn x n:
  inc n Bnat ->
  inc x (Bint n) -> inc (succ x) (Bint (succ n)).
Proof.
move => nB.
move/(BintP nB) => lin.
apply /(BintsP nB); apply /card_le_succ_lt0P => //; co_tac.
Qed.

Lemma inc0_int01: inc \0c (Bint \1c).
Proof. by apply /(BintP); fprops; apply: card_lt_01. Qed.

Lemma inc0_int02: inc \0c (Bint \2c).
Proof. by apply /(BintP); fprops; apply: card_lt_02. Qed.

Lemma cardinal_c_induction5 (r:property) a:
  inc a Bnat -> r \0c ->
  (forall n, n <c a -> r n -> r (succ n))
  -> (forall n, n <=c a -> r n).
Proof.
move=> aB r0 rs.
have rss: forall n,
  inc n (Bint a) -> r n -> r (succ n).
  by move=> n /(BintP aB); apply: rs.
move: (cardinal_c_induction3_v (r:=r) BS0 aB r0 rss) => h n na.
by apply: h; apply /(BintcP aB).
Qed.

Section IntervalBnatwo.
Variables (a b: Set).
Hypotheses (aB:inc a Bnat)(bB:inc b Bnat).

Lemma Binto_wor: worder_on (Bint_cco a b) (Bintcc a b).
Proof.
move: cardinal_le_wor => wo.
have r: (forall x, inc x (interval_cc Bnat_order a b) -> x <=c x).
  move=> x xb; exact (card_leR (CS_Bnat (Bint_S xb))).
by move: (wordering_pr wo r).
Qed.

Lemma Binto_gleP x y:
  gle (Bint_cco a b) x y <->
    [/\ inc x (Bintcc a b), inc y (Bintcc a b) & x <=c y].
Proof. apply: graph_on_P1. Qed.

Lemma Binto_gleP2 x y:
  gle (Bint_cco a b) x y <-> [/\ a <=c x, y <=c b & x <=c y].
Proof.
split.
  move/Binto_gleP=> [] /(Bint_ccP1 aB bB) [pa pb] /(Bint_ccP1 aB bB) [pc pd] pe.
  done.
move => [pa pb pc]; apply/Binto_gleP; split => //;
  apply /(Bint_ccP1 aB bB); split => //; co_tac.
Qed.

End IntervalBnatwo.

Definition Bint_co a :=
  graph_on cardinal_le (Bint a).

Section IntervalBnatwo1.
Variable (a: Set).
Hypothesis (aB:inc a Bnat).

Lemma Bintco_wor: worder_on (Bint_co a) (Bint a).
Proof.
move: cardinal_le_wor => wo.
have r: forall x, inc x (Bint a) -> x <=c x.
  move=> x xi; move: (Bint_S1 xi) => xB; fprops.
by move: (wordering_pr wo r).
Qed.

Lemma Bintco_gleP x y: (gle (Bint_co a) x y <-> (x <=c y /\ y <c a)).
Proof.
split.
  by move /graph_on_P1 => [] /(BintP aB) xa /(BintP aB) ya xy.
move=> [xy ya]; apply/graph_on_P1; split => //;
  apply /(BintP aB) => //; co_tac.
Qed.

End IntervalBnatwo1.

Lemma segment_Bnat_order x: inc x Bnat ->
  segment Bnat_order x = interval_co Bnat_order \0c x.
Proof.
move=> xB; set_extens t; move /Zo_P => [pa pb];apply:Zo_i => //.
  move: pb => [] /Bnat_order_leP [tn aa bb] cc.
  split; first by apply/Bnat_order_leP; split; fprops.
  split; first by apply/Bnat_order_leP; split; fprops.
  exact.
by case: pb.
Qed.

Definition rest_plus_interval a b :=
  Lf(fun z => z +c b)(Bintcc \0c a) (Bintcc b (a +c b)).

Definition rest_minus_interval a b :=
  Lf(fun z => z -c b) (Bintcc b (a +c b)) (Bintcc \0c a).

Theorem restr_plus_interval_is a b: inc a Bnat -> inc b Bnat->
 [/\ bijection (rest_plus_interval a b) ,
   bijection (rest_minus_interval a b),
   (rest_minus_interval a b) = inverse_fun (rest_plus_interval a b) &
   order_isomorphism (rest_plus_interval a b)
  (Bint_cco \0c a)
  (Bint_cco b (a +c b))].
Proof.
move=> aB bB.
move: BS0 => zB.
move: (BS_sum aB bB) => abB.
set E1:= Bintc a.
set E2:= Bintcc b (a +c b).
have tap: lf_axiom (fun z => z +c b) E1 E2.
  move => z /(BintcP aB) za; apply/(Bint_ccP1 bB abB); split.
    rewrite csumC; apply: csum_M0le; fprops.
  apply: csum_Mlele=>//; fprops.
have tam: lf_axiom (fun z => z -c b) E2 E1.
  move => z /(Bint_ccP1 bB abB) [bt tab]; apply /(BintcP aB).
  move: (BS_diff b (BS_le_int tab abB)) => sB; apply: cdiff_increasing2 =>//.
set (f:= rest_plus_interval a b).
set (g:= rest_minus_interval a b).
have ff:function f by apply: lf_function.
have fg:function g by apply: lf_function.
have sf:source f = target g by rewrite lf_source lf_target.
have sg:source g = target f by rewrite lf_source lf_target.
have cfg:f \coP g by [].
have cgf: g \coP f by [].
have c1: g \co f = identity (source f).
  apply: function_exten; [fct_tac | fprops | aw | symmetry; aw | ].
  rewrite compf_s;move=> x xsf /=.
  rewrite (identity_V xsf); aw.
  move: xsf; rewrite lf_source=> xs.
  rewrite (lf_V tap xs) (lf_V tam (tap _ xs)).
  rewrite cdiff_pr1 =>//; apply: (Bint_S xs).
have c2: f \co g = identity (source g).
  apply: function_exten ; [fct_tac | fprops | aw | symmetry; aw | ].
  rewrite compf_s;move=> x xsg /=.
  rewrite (identity_V xsg) (compf_V cfg xsg).
  move: xsg; rewrite lf_source=> xs.
  rewrite (lf_V tam xs).
  have xB: inc x Bnat by apply :(Bint_S xs).
  move: xs => /(Bint_ccP1 bB abB) [bx xaB].
  have aux: inc (x -c b) (Bintcc \0c a).
    apply/(BintcP aB); apply: cdiff_increasing2 =>//.
  rewrite (lf_V tap aux) csumC cdiff_pr //.
move: (bijective_from_compose cgf cfg c1 c2)=> [bf bg gif]; split => //.
have sp : E1 = source (rest_plus_interval a b).
  by rewrite /rest_plus_interval; aw.
move: (Binto_wor \0c a) => [[o1 _ ] sr1].
move: (Binto_wor b (a +c b))=> [[o2 _ ] sr2].
red;rewrite /bijection_prop sr1 sr2 lf_source lf_target;split => //.
move=> x y /=; rewrite lf_source => xsf ysf.
rewrite (lf_V tap xsf) (lf_V tap ysf).
apply: (iff_trans (Binto_gleP \0c a x y)).
symmetry.
apply (iff_trans (Binto_gleP b (a +c b) (x +c b) (y +c b))).
split; move => [pa [pb pc]];split => //; try (apply: tap => //).
  apply: (csum_le_simplifiable bB (Bint_S xsf) (Bint_S ysf)).
  by rewrite csumC (csumC b y).
apply: csum_Mlele=>//; fprops.
Qed.

Lemma card_Bintc a: inc a Bnat ->
  cardinal (Bintc a) = succ a.
Proof.
move: a; apply: cardinal_c_induction.
  rewrite succ_zero Bint_cc00; apply: cardinal_set1.
move => n nB.
move: (BS_succ nB) => snB.
rewrite (Bint_co_cc nB) (Bint_co_cc snB).
have [<- aux]:= (Bint_pr4 snB).
by rewrite card_succ_pr ; [move => -> |].
Qed.

Lemma Bint_pr1 a: inc a Bnat -> a <> \0c ->
  Bintcc \0c (cpred a) = Bint a.
Proof.
move: BS0 => zB.
move=> aB naz;move: (cpred_pr aB naz) => [fp ass].
rewrite {2} ass - Bint_co_cc //.
Qed.

Lemma card_Bintcp a: inc a Bnat -> a <> \0c ->
  cardinal (Bintc (cpred a)) = a.
Proof.
move=> aB naz.
by move: (cpred_pr aB naz) => [fp ass]; rewrite card_Bintc.
Qed.

Lemma card_Bint a: inc a Bnat ->
  cardinal (Bint a) = a.
Proof.
move=> aB; case: (equal_or_not a \0c).
  move => ->; rewrite Bint_co00; apply: cardinal_set0.
move=> h; rewrite - Bint_pr1//; apply: card_Bintcp=>//.
Qed.

Theorem card_Bintcc a b: a <=N b ->
  cardinal (Bintcc a b) = succ (b -c a).
Proof.
move=> [aB bB ab].
move: (cdiff_pr ab) (BS_diff a bB) => aux cB.
rewrite csumC in aux.
set (c:= b -c a) in *.
move: (restr_plus_interval_is cB aB) => [b1 _ _ _].
have eq: (Bintcc \0c c) \Eq (Bintcc a b).
  exists (rest_plus_interval c a); rewrite /rest_plus_interval.
  red;rewrite lf_source lf_target; split => //; ue.
by rewrite -(card_Bintc cB); apply /card_eqP; eqsym.
Qed.

Lemma card_Bint1c a: inc a Bnat ->
  cardinal (Bint1c a) = a.
Proof.
move => aB.
case: (equal_or_not a \0c).
  move=> ->.
  have ->: (Bint1c \0c = emptyset).
    rewrite /Bint1c.
    apply /set0_P => y; move /(Bint1cPb BS0)=> [c1y cy0].
    move: (card_leT c1y cy0) card_lt_01 => h1 h2;co_tac.
  apply: cardinal_set0.
move => anz.
have aux1: \1c <=c a by apply: card_ge1; fprops.
have aux: \1c <=N a by split;fprops.
have so: inc (a -c \1c) Bnat by move: BS1 => i1; fprops.
rewrite card_Bintcc // Bsucc_rw // csumC.
apply: cdiff_pr; fprops.
Qed.

Lemma finite_Bintcc a b: finite_set (Bintcc a b).
Proof.
apply/card_finite_setP.
case: (p_or_not_p (a <=N b)) => h.
  rewrite card_Bintcc //; move: h => [aB bB _]; fprops.
have ->: (Bintcc a b) = emptyset.
   apply /set0_P => t /Zo_hi [] /Bnat_order_leP [pa _ pc]
      /Bnat_order_leP [_ pe pf].
   case: h; split;fprops; co_tac.
rewrite cardinal_set0; fprops.
Qed.

Lemma finite_Bint a: finite_set (Bint a).
Proof.
have aux:sub (Bint a) (Bintcc \0c a).
   by move => t /Zo_P [pa [pb [pc _]]]; apply /Zo_P.
have : (finite_set (Bintcc \0c a)) by apply: finite_Bintcc.
apply: (sub_finite_set aux).
Qed.

Lemma infinite_Bnat_alt: ~(finite_set Bnat).
Proof.
move /BnatP =>h.
move: (sub_smaller (Bint_S (a:=\0c) (b:=cardinal Bnat))).
rewrite (card_Bintc h).
by move /(card_le_succ_ltP _ h) => [_].
Qed.

Lemma isomorphism_worder_finite r r':
  total_order r -> total_order r' ->
  finite_set (substrate r) -> (substrate r) \Eq (substrate r') ->
  exists! f, order_isomorphism f r r'.
Proof.
move=> tor tor' fs.
move /card_eqP => sc.
have fs': finite_set (substrate r') by red; rewrite - sc.
move:(finite_set_torder_wor tor fs) (finite_set_torder_wor tor' fs').
move => wor wor'; move: (isomorphism_worder wor wor') => iw.
have aux: forall u v f, order_isomorphism f u v ->
   segmentp v (range (graph f)) /\ order_morphism f u v.
  move => f u v h; split; last by apply:order_isomorphism_w.
  move: h => [_ or' [[injf sjf] sf tf] pf].
  by rewrite (surjective_pr3 sjf) tf; apply: substrate_segment.
case: iw.
  move => [f [[pa mf] pc]]; exists f; split.
    move: (order_morphism_fi mf) => injf.
    move: mf => [o1 o2 [ff sf tf] pf]; split => //; split => //.
    apply: bijective_if_same_finite_c_inj; [ by rewrite sf tf | ue| exact].
 by move => f' xx; apply:pc; apply: aux.
move => [f [[pa mf] pc]].
have oi: (order_isomorphism f r' r).
  move: (order_morphism_fi mf) => injf.
  move: mf => [o1 o2 [ff sf tf] pf].
   have bf: bijection f by apply: bijective_if_same_finite_c_inj;
     rewrite ? sf ?tf;[ symmetry; apply: sc| exact| exact].
   split=> //.
move: (inverse_order_is oi)=> oii.
exists (inverse_fun f); split => //.
move => f' h1.
rewrite (pc _ (aux _ _ _ (inverse_order_is h1))).
move: h1 => [_ _ [[[ff _] _] _ _] _ ].
by rewrite (ifun_involutive ff).
Qed.

Theorem finite_ordered_interval r: total_order r ->
  finite_set (substrate r) ->
  exists! f, order_isomorphism f r
    (Bint_cco \1c (cardinal (substrate r))).
Proof.
move=> tot fs.
move: (fs); move/BnatP => fs'.
move: (Binto_wor \1c (cardinal (substrate r))) => [pa pb].
move: (card_Bint1c fs').
move/card_eqP;rewrite /Bint1c - pb; fprops.
move => h;apply: (isomorphism_worder_finite tot (worder_total pa) fs).
by eqsym.
Qed.

Theorem finite_ordered_interval1 r: total_order r ->
  finite_set (substrate r) ->
  exists !f, order_isomorphism f r
    (Bint_co (cardinal (substrate r))).
Proof.
move=> tor fs.
move: (finite_set_torder_wor tor fs)=> wor.
move: (fs) => /BnatP fs'.
move: (card_Bint fs') => /card_eqP.
rewrite - (proj2 (Bintco_wor _)) // => e.
move: (worder_total (proj1(Bintco_wor (cardinal (substrate r))))) => tor'.
by apply: (isomorphism_worder_finite tor tor' fs); eqsym.
Qed.

A finite sum or product can be defined by induction

Lemma induction_on_sum a f: inc a Bnat ->
  let iter := fun n=> card_sumb (Bint n) f
    in (iter a) +c (f a) = (iter (succ a)).
Proof.
move=> aB /=.
by move: (Bint_pr4 aB) => [<- aux];symmetry; apply csumA_setU1.
Qed.

Lemma induction_on_prod a f: inc a Bnat ->
  let iter := fun n=> card_prodb (Bint n) f
    in (iter a) *c (f a) = (iter (succ a)).
Proof.
move=> aB /=.
move: (Bint_pr4 aB) => [<- aux].
by symmetry; apply cprodA_setU1.
Qed.

Lemma fct_sum_rec0 f n: inc n Bnat ->
  card_sumb (Bintc n) f = (card_sumb (Bint1c n) f) +c (f \0c).
Proof.
move=> nB; move: (Bint_pr5 nB) => [<- aux].
by apply csumA_setU1.
Qed.

Lemma fct_sum_rec1 f n: inc n Bnat ->
  card_sumb (Bintcc \0c (succ n)) f
  = (card_sumb (Bintcc \0c n) (fun i=> f (succ i))) +c (f \0c).
Proof.
move=> nB.
have sB:inc (succ n) Bnat by fprops.
rewrite (fct_sum_rec0 _ sB); congr (_ +c (f \0c)).
set i1:= Bint1c _ ; set i0:= Bintcc _ _.
have p1: forall x : Set, inc x i0 -> inc (succ x) i1.
  move => t /(BintcP nB) => tn; apply /(Bint1cP sB).
  have ct: cardinalp t by co_tac.
  split; [ apply: succ_nz | apply/ (card_le_succ_succP ct )]; fprops.
rewrite /card_sumb (csum_Cn2 (I:=i0) (f:= succ)).
   congr (card_sum _); apply: Lg_exten; move=> x xi0 /=; bw; apply: p1=>//.
split => //.
    by move=> x xi; bw; apply: p1.
 move=> u v ui vi susv; apply: succ_injective1.
     move: (Bint_S ui); fprops.
   move: (Bint_S vi); fprops.
   done.
move=> y; bw; move/(Bint1cP sB) => [nyz le_s].
have fy:inc y Bnat by Bnat_tac.
move: (cpred_pr fy nyz)=> [pB ns].
exists (cpred y) => //.
apply/(BintcP nB); apply/card_le_succ_succP => //; fprops; ue.
Qed.

Lemma fct_sum_rev f n: inc n Bnat ->
  let I := (Bint (succ n)) in
  card_sumb I f = card_sumb I (fun i=> f (n -c i)).
Proof.
move=> nB I.
have snB: inc (succ n) Bnat by fprops.
set X := Lg I f.
pose g i := n -c i.
have p1: forall x, inc x I -> inc (n -c x) I.
  move=> x /(BintsP nB) => xn; apply /(BintsP nB).
  apply: cdiff_le_symmetry =>//.
rewrite /card_sumb.
have->:(Lg I (fun i : Set => f (n -c i)) = Lg I (fun z => Vg X (g z))).
  apply: Lg_exten; move=> x xI; rewrite /X /g; bw; apply: p1 =>//.
apply: csum_Cn2; split => //.
    rewrite /g/X; bw.
  move=> x y /(BintsP nB) xn /(BintsP nB) yn; rewrite /g => h.
  by rewrite - (double_diff nB xn) -(double_diff nB yn) h.
rewrite /g; bw => y /(BintsP nB) yn; rewrite -(double_diff nB yn).
exists (n -c y) => //; apply /(BintsP nB).
apply: cdiff_le_symmetry =>//; Bnat_tac.
Qed.

EIII-5-4 Finite sequences

EIII-5-5 Characteristic functions on sets


Lemma char_fun_V_aa A x: inc x A ->
  Vf (char_fun A A) x = \1c.
Proof. by move => xa; rewrite char_fun_V_a. Qed.

Lemma char_fun_V_bb A x: inc x A ->
  Vf (char_fun emptyset A) x = \0c.
Proof.
move => xa; rewrite char_fun_V_b; fprops.
by apply /setC_P; split => // /in_set0.
Qed.

Lemma char_fun_constant A B:
   sub A B -> (cstfp (char_fun A B) B) -> (A=B \/ A = emptyset).
Proof.
move=> AB p.
case: (emptyset_dichot A); [by right | move=> [u uA]; left ].
apply: extensionality=>// t tB.
ex_middle v.
have xc:inc t (B -s A) by apply /setC_P; split =>//.
case: card1_nz.
by rewrite - (char_fun_V_b AB xc)- (char_fun_V_a AB uA) (p _ _ (AB _ uA) tB).
Qed.

Lemma char_fun_setC A B x: sub A B -> inc x B ->
  Vf (char_fun (B -s A) B) x = \1c -c (Vf (char_fun A B) x).
Proof.
move=> AB xB.
have sc:sub (B -s A) B by apply: sub_setC.
case: (inc_or_not x A).
  move=> xA; rewrite char_fun_V_b //.
    rewrite char_fun_V_a //; symmetry; apply: cdiff_n_n; fprops.
  by rewrite setC_K.
move=> h.
have xc: inc x (B -s A) by apply/setC_P.
rewrite char_fun_V_a // char_fun_V_b //.
symmetry;apply: cdiff_n_0; fprops.
Qed.

Lemma char_fun_setI A A' B x: sub A B -> sub A' B -> inc x B ->
  Vf (char_fun (A \cap A') B) x
  = (Vf (char_fun A B) x) *c (Vf (char_fun A' B) x).
Proof.
move=> AB A'B xB.
have Ha:sub (A \cap A') B.
  by move=> t /setI2_P [tA _]; apply: AB.
case: (inc_or_not x A) => h.
  have cW:cardinalp (Vf (char_fun A' B) x) by apply: char_fun_V_cardinal.
  rewrite (char_fun_V_a AB h) cprod1l //.
  case: (inc_or_not x A') => xA.
    have aux:inc x (A \cap A') by apply: setI2_i.
    rewrite char_fun_V_a // char_fun_V_a //.
  have aux:inc x (B -s (A \cap A'))
    by apply /setC_P;split => //; move /setI2_P =>[_].
  rewrite char_fun_V_b // char_fun_V_b //.
  by apply /setC_P.
have aux: inc x (B -s (A \cap A'))
 by apply /setC_P;split => //; move /setI2_P =>[].
have aux2:inc x (B -s A) by fprops.
by rewrite char_fun_V_b // char_fun_V_b // cprodC cprod0r.
Qed.

Lemma char_fun_setU A A' B x: sub A B -> sub A' B -> inc x B ->
  (Vf (char_fun (A \cap A') B) x)
  +c (Vf (char_fun (A \cup A') B) x)
  = (Vf (char_fun A B) x) +c (Vf (char_fun A' B) x).
Proof.
move=> AB A'B xB.
have Ha:sub (A \cap A') B by move=> t /setI2_P [ta _]; apply: AB.
have Hb:sub (A \cup A') B by move=> t /setU2_P; case; fprops.
case: (p_or_not_p (inc x A))=> xA.
  rewrite (char_fun_V_a AB xA).
  rewrite (char_fun_V_a Hb (setU2_1 A' xA)).
  case: (p_or_not_p (inc x A'))=> xA'.
    rewrite (char_fun_V_a A'B xA') char_fun_V_a //.
     by apply: setI2_i.
  rewrite csumC; apply: f_equal.
  by rewrite ! char_fun_V_b //; apply /setC_P; split => //; move /setI2_P => [].
have Hc: inc x (B -s A) by fprops.
have Hd:inc x (B -s (A \cap A')).
  by apply /setC_P; split => //; move /setI2_P => [].
rewrite (char_fun_V_b AB Hc) (char_fun_V_b Ha Hd).
case: (p_or_not_p (inc x A')) => aux.
  have xu: inc x (A \cup A') by apply: setU2_2.
  by rewrite (char_fun_V_a Hb xu) (char_fun_V_a A'B aux).
have xc:inc x (B -s (A \cup A')).
  by apply /setC_P; split => //;move /setU2_P => [].
have xba: inc x (B -s A') by fprops.
by rewrite (char_fun_V_b Hb xc) (char_fun_V_b A'B xba).
Qed.

EIII-5-6 Euclidean Division


Lemma least_int_prop (prop:property):
  (forall x, prop x -> inc x Bnat) -> (exists x, prop x) ->
  prop \0c \/ (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_P [_].
right; move: q=> [a [aB /Zo_hi psa /Zo_P h]]; ex_tac;fprops.
Qed.

Lemma least_int_prop1 (prop:property):
  (forall x, prop x -> inc x Bnat) -> ~(prop card_zero) ->
  (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.

Definition card_division_prop a b q r :=
  a = (b *c q) +c r /\ r <c b.

Lemma card_division_prop_alt a b q r: inc a Bnat-> inc b Bnat ->
  inc q Bnat-> inc r Bnat -> b <> \0c ->
  (card_division_prop a b q r <->
  [/\ (b *c q) <=c a, a <c (b *c succ q) & r = a -c (b *c q)]).
Proof.
move=> aB bB qB rB nzb; rewrite /card_division_prop.
set (w:= b *c q).
rewrite Bsucc_rw // cprodC cprod_sumDr cprodC cprod1l; fprops.
have wB: inc w Bnat by rewrite /w; fprops.
split.
  move=> [av lt];split => //.
  - rewrite av; apply: csum_M0le; fprops.
  - rewrite av; apply: csum_Mlelt; fprops.
  - by symmetry;apply: cdiff_pr2 =>//; symmetry; rewrite csumC.
move=> [lwa ltas rv].
rewrite rv.
have aux: inc (b *c q +c b) Bnat by fprops.
split; first by symmetry; apply: cdiff_pr =>//.
move: ltas => /(card_ltP aB aux) [c [cB nzc s]] {aux}.
move: (cdiff_pr lwa); rewrite -rv=> aux.
apply /(card_ltP rB bB); ex_tac.
apply: (@csum_simplifiable_left w);fprops.
by rewrite csumA aux.
Qed.

Lemma card_division_unique a b q r q' r': inc a Bnat-> inc b Bnat ->
  inc q Bnat-> inc r Bnat -> inc q' Bnat-> inc r' Bnat -> b <> \0c ->
  card_division_prop a b q r -> card_division_prop a b q' r' ->
  (q = q' /\ r =r').
Proof.
move=> aB bB qB rB q'B r'B nbz.
move /(card_division_prop_alt aB bB qB rB nbz)=> [le1 lt1 e1].
move /(card_division_prop_alt aB bB q'B r'B nbz)=> [le2 lt2 e2].
suff : q = q' by move=> h; split => //; rewrite e1 e2 h.
move: (card_le_ltT le1 lt2) => lt3.
move: (card_le_ltT le2 lt1) => lt4.
move: (cprod_lt_simplifiable bB q'B (BS_succ qB) nbz lt4).
move: (cprod_lt_simplifiable bB qB (BS_succ q'B) nbz lt3).
move /(card_lt_succ_leP q'B) => pa /(card_lt_succ_leP qB) => pb; co_tac.
Qed.

Lemma card_division_exists a b: inc a Bnat-> inc b Bnat ->
  b <> \0c -> exists q r,
    [/\ inc q Bnat, inc r Bnat & card_division_prop a b q r].
Proof.
move=> aB bB nzb.
set (pp:= fun q => inc q Bnat /\ a <c (b *c q)).
have np: (forall x, pp x -> inc x Bnat) by move => x [].
have zp: (~ (pp \0c)).
   rewrite /pp; move => [_]; rewrite cprod0r.
   move=> h;apply: (card_lt0 h).
have ep: (exists x, pp x).
  rewrite /pp; exists (succ a); split; first by fprops.
  have aux: (succ a) <=c (b *c (succ a)).
     by rewrite cprodC; apply: Bprod_M1le; fprops.
  by apply /card_le_succ_ltP.
move: (least_int_prop1 np zp ep)=> [q [qB q1 q2]].
have p1: ((b *c q) <=c a).
  move: (Bnat_to_el (BS_prod bB qB) aB); case => //.
  move=> [p1 p2]; case: q2; split; [exact | split ] =>//.
move: (cdiff_pr p1); set (r:= a -c (b *c q)) => rp.
have rB: inc r Bnat by rewrite /r; apply: (BS_diff _ aB).
exists q; exists r; split => //; apply /card_division_prop_alt => //.
by split => //; move: q1=> [_].
Qed.

Definition card_quo a b := least_ordinal (fun q => a <c b *c (succ q)) a.
Definition card_rem a b := a -c (b *c (card_quo a b)).
Definition card_divides b a :=
  [/\ inc a Bnat, inc b Bnat & card_rem a b = \0c].

Notation "x %/c y" := (card_quo x y) (at level 40).
Notation "x %%c y" := (card_rem x y) (at level 40).
Notation "x %|c y" := (card_divides x y) (at level 40).

Lemma cquo_zero a: a %/c \0c = \0c.
Proof.
rewrite /card_quo /least_ordinal.
set s := Zo _ _.
have -> : s = emptyset.
  apply /set0_P => y /Zo_hi; rewrite cprodC cprod0r; apply: card_lt0.
by rewrite setI_0.
Qed.

Lemma card_division a b (q := a %/c b) (r := (a %%c b)):
  inc a Bnat -> inc b Bnat -> b <> \0c ->
  [/\ inc q Bnat, inc r Bnat & card_division_prop a b q r].
Proof.
move=> aB bB bnz.
pose p z := (a <c b *c succ z).
have ca: cardinalp a by fprops.
have oa: ordinalp a by apply:OS_cardinal.
have pa: p a.
 have aux: (succ a) <=c (b *c (succ a)).
     by rewrite cprodC; apply: Bprod_M1le; fprops.
  by apply /card_le_succ_ltP.
move: (least_ordinal1 oa pa); rewrite /p -/q.
move=> [qa qb qc].
have qd: q <=o a by split => //; exact (qc _ oa pa).
have qB: inc q Bnat.
  case: (equal_or_not q a); first by move => ->.
  move=> naq.
  have: q <o a by split.
  move /ord_ltP0 => [_ _ qe].
  move /BnatP: aB => aB; apply /BnatP;exact: (finite_o_increasing qe aB).
have rB: inc r Bnat by apply: BS_diff => //; apply: BS_prod.
split => //.
apply /card_division_prop_alt => //; split => //.
case: (p_or_not_p (q = \0c)).
  move=> ->; rewrite cprod0r; apply: czero_least; fprops.
move=> qnz; move: (cpred_pr qB qnz); set (z := (cpred q)).
move => [zB qs].
case: (card_le_to_el (CS_prod2 b q) ca) => //; rewrite qs => h.
have oz: ordinalp z by apply:OS_cardinal; fprops.
move: (qc _ oz h) => qz.
have zq : inc z q.
  have fz: finite_c z by fprops.
  rewrite qs (succ_of_finite fz) /succ_o; fprops.
case: (ordinal_irreflexive oz (qz _ zq)).
Qed.

Lemma crem_zero a: inc a Bnat -> a %%c \0c = a.
Proof. move => h; rewrite /card_rem cprodC cprod0r cdiff_n_0 //. Qed.

Lemma BS_quo a b: inc a Bnat-> inc b Bnat ->
  inc (a %/c b) Bnat.
Proof.
move => aB bB.
case: (equal_or_not b \0c) => bnz.
  rewrite bnz cquo_zero;fprops.
exact: (proj31 (card_division aB bB bnz)).
Qed.

Lemma BS_rem a b: inc a Bnat-> inc b Bnat ->
  inc (a %%c b) Bnat.
Proof.
move => aB bB.
case: (equal_or_not b \0c) => bnz.
  rewrite bnz crem_zero //.
exact: (proj32 (card_division aB bB bnz)).
Qed.

Hint Resolve BS_rem BS_quo: fprops.

Lemma cdiv_pr a b: inc a Bnat-> inc b Bnat ->
  a = (b *c (a %/c b)) +c (a %%c b).
Proof.
move => aB bB.
case: (equal_or_not b \0c) => bnz.
  rewrite bnz (crem_zero aB) cquo_zero cprod0r; aw; fprops.
by move: (card_division aB bB bnz) =>[_ _ [h _]].
Qed.

Lemma crem_pr a b: inc a Bnat-> inc b Bnat -> b <> \0c ->
  (a %%c b) <c b.
Proof.
by move => aB bB bnz; move: (card_division aB bB bnz) =>[_ _ [_]].
Qed.

Lemma cquorem_pr a b q r:
  inc a Bnat-> inc b Bnat -> inc q Bnat -> inc r Bnat ->
  card_division_prop a b q r -> (q = a %/c b /\ r = a %%c b).
Proof.
move => aB bB qB rB p'.
case: (equal_or_not b \0c) => bnz.
  move: p' => [_ ]; rewrite bnz =>h; case: (card_lt0 h).
move: (card_division aB bB bnz)=> [qqB rrB p].
apply: (card_division_unique aB bB qB rB qqB rrB bnz p' p).
Qed.

Lemma cquorem_pr0 a b q:
  inc a Bnat-> inc b Bnat -> inc q Bnat -> b <> \0c ->
   a = (b *c q) -> (q = a %/c b /\ \0c = a %%c b).
Proof.
move => aB bB qB bnz p'.
apply: cquorem_pr =>//.
  fprops.
red; rewrite -p' (bsum0r aB).
split; [ trivial | split; [ apply: czero_least | ]]; fprops.
Qed.

Lemma cdivides_pr a b:
  b %|c a -> a = b *c (a %/c b).
Proof.
move => [aB bB dv].
move: (cdiv_pr aB bB); rewrite dv.
by rewrite (bsum0r (BS_prod bB (BS_quo aB bB))).
Qed.

Lemma cdivides_pr1 a b: inc a Bnat -> inc b Bnat ->
  b %|c (b *c a).
Proof.
move=> aB bB.
move: (BS_prod bB aB) => pB.
split => //.
case: (equal_or_not b card_zero) => bnz.
  rewrite bnz cprodC cprod0r crem_zero //; fprops.
by case: (cquorem_pr0 pB bB aB bnz (refl_equal (b *c a))).
Qed.

Lemma cdivides_pr2 a b q:
  inc a Bnat -> inc b Bnat -> inc q Bnat -> b <> \0c ->
  a = b *c q -> q = a %/c b.
Proof.
move => aB bB qB nzb abq.
by case: (cquorem_pr0 aB bB qB nzb abq).
Qed.

Lemma cdivides_one a: inc a Bnat -> \1c %|c a.
Proof.
move=> aB; rewrite - (cprod1l (CS_Bnat aB)).
apply: (cdivides_pr1 aB BS1).
Qed.

Lemma cquo_one a: inc a Bnat -> a %/c \1c = a.
Proof.
move=> aB; symmetry; apply: cdivides_pr2; fprops; fprops.
rewrite cprod1l;fprops.
Qed.

Lemma cdivides_pr3 a b q:
   b %|c a -> q = a %/c b -> a = b *c q.
Proof. by move => H aux; move: (cdivides_pr H); rewrite -aux.
Qed.

Lemma cdivides_pr4 b q: inc b Bnat -> inc q Bnat -> b <> \0c ->
   (b *c q) %/c b = q.
Proof. move=> *; symmetry; apply: cdivides_pr2 =>//; fprops.
Qed.

Lemma cdivision_itself a: inc a Bnat -> a <> \0c ->
  (a %|c a /\ a %/c a = \1c).
Proof.
move=> aB anz; rewrite /card_divides.
have aux:a = a *c \1c by rewrite (cprod1r (CS_Bnat aB)).
by move: (cquorem_pr0 aB aB BS1 anz aux) => [p1 p2].
Qed.

Lemma cdivides_itself a: inc a Bnat -> a <> \0c ->
   a %|c a.
Proof. by move=> aB anz; move: (cdivision_itself aB anz) => [h _]. Qed.

Lemma cquo_itself a: inc a Bnat -> a <> \0c ->
   a %/c a = \1c.
Proof. by move=> aB anz; move: (cdivision_itself aB anz) => [ _ h]. Qed.

Lemma cdivision_of_zero a: inc a Bnat ->
  (a %|c \0c /\ \0c %/c a = \0c).
Proof.
move=> aB; rewrite /card_divides.
move: BS0 => bs0.
have aux: \0c = a *c \0c by rewrite cprod0r.
case: (equal_or_not a \0c) => anz.
  by rewrite anz cquo_zero crem_zero.
by move: (cquorem_pr0 BS0 aB BS0 anz aux) => [p1 p2].
Qed.

Lemma cdivides_trans a b a':
  a %|c a'-> b %|c a -> b %|c a'.
Proof.
move=> d1 d2.
rewrite (cdivides_pr d1) {1} (cdivides_pr d2) - cprodA.
move: d1 d2 => [p1 p2 _] [p3 p4 _].
apply: cdivides_pr1 =>//; fprops.
Qed.

Lemma cdivides_trans1 a b a':
  a %|c a' -> b %|c a
  -> a' %/c b = (a' %/c a) *c (a %/c b).
Proof.
move=> d1 d2.
move: (cdivides_pr d1).
rewrite {1} (cdivides_pr d2) - cprodA => h.
case: (equal_or_not b \0c) => bnz.
 by rewrite bnz cquo_zero cquo_zero cprod0r.
move: d1 d2 => [a'B aB _][_ bB _].
have pB: inc ((a %/c b) *c (a' %/c a)) Bnat by fprops.
rewrite - (cdivides_pr2 a'B bB pB bnz h).
by rewrite cprodC.
Qed.

Lemma cdivides_trans2 a b c: inc c Bnat ->
  b %|c a-> b %|c (a *c c).
Proof.
move=> cB ba.
have aB: (inc a Bnat) by move: ba => [h _].
move: (cdivides_pr1 cB aB) => aux.
apply: (cdivides_trans aux ba).
Qed.

Lemma cquo_simplify a b c:
  inc a Bnat -> inc b Bnat -> inc c Bnat -> b <> \0c -> c <> \0c ->
  (a *c c) %/c (b *c c) = a %/c b.
Proof.
move=> aB bB cB bnz cnz.
move: (card_division aB bB bnz)=> [qB rB []].
set q:= (a %/c b); set r := a %%c b.
move=> e1 lrb; symmetry.
move: (BS_prod aB cB)(BS_prod bB cB)(BS_prod (BS_rem aB bB) cB) => p1 p2 p3.
have dv: (card_division_prop (a *c c) (b *c c) q (r *c c)).
  split.
     rewrite (cprodC b c) - cprodA (cprodC c _).
    by rewrite - cprod_sumDr e1.
  rewrite (cprodC b c) cprodC.
  apply: cprod_Mlelt =>//; fprops.
by move: (cquorem_pr p1 p2 qB p3 dv) => [res _].
Qed.

Lemma cdivides_and_sum a a' b: b %|c a -> b %|c a'
  -> (b %|c (a +c a') /\
    (a +c a') %/c b = (a %/c b) +c (a' %/c b)).
Proof.
move=> d1 d2.
move: (cdivides_pr d1)(cdivides_pr d2)=> am bm.
set s := (a %/c b) +c (a' %/c b).
have ->: (a +c a' = b *c s).
  by rewrite /s cprod_sumDl -am -bm.
move: d1 d2 => [aB bB _][a'B _ _].
have sB:inc s Bnat by rewrite /s; fprops.
split; first by apply: cdivides_pr1 =>//.
case: (equal_or_not b \0c) => bs.
  rewrite {2} /s bs ! cquo_zero; aw; fprops.
by symmetry; apply: (cdivides_pr2 (BS_prod bB sB) bB sB bs).
Qed.

Lemma cdistrib_prod2_sub a b c: inc a Bnat -> inc b Bnat -> inc c Bnat
  -> c <=c b ->
  a *c (b -c c) = (a *c b) -c (a *c c).
Proof.
move=> aB bB cB le; symmetry; apply: cdiff_pr2; fprops.
rewrite - cprod_sumDl csumC cdiff_pr //.
Qed.

Lemma cdivides_and_difference a a' b:
  a' <=c a -> b %|c a -> b %|c a'
  -> [/\ b %|c (a -c a'), (a' %/c b) <=c (a %/c b) &
    (a -c a') %/c b = (a %/c b) -c (a' %/c b)].
Proof.
move=> le d1 d2.
move: (cdivides_pr d1)(cdivides_pr d2)=> am bm.
set s := (a %/c b) -c (a' %/c b).
move: d1 d2 => [aB bB _][a'B _ _].
move: (BS_quo aB bB)(BS_quo a'B bB) => q1 q2.
have q3: (a' %/c b) <=c (a %/c b).
  case: (equal_or_not b \0c) => bnz.
    rewrite bnz ! cquo_zero; fprops.
  rewrite am bm in le.
  apply: (cprod_le_simplifiable bB q2 q1 bnz le).
have ->: (a -c a' = b *c s).
  by rewrite /s cdistrib_prod2_sub // -am -bm.
have sB:inc s Bnat by rewrite /s; fprops.
split => //; first by apply: cdivides_pr1 =>//.
case: (equal_or_not b card_zero) => bs.
  rewrite {2} /s bs ! cquo_zero cdiff_n_n; fprops.
by symmetry; apply: (cdivides_pr2 (BS_prod bB sB) bB sB bs).
Qed.

EIII-5-7 Expansion to base b


Lemma b_power_k_large a b: inc a Bnat -> inc b Bnat ->
  \1c <c b -> a <> \0c -> exists k,
    [/\ inc k Bnat, (b ^c k) <=c a & a <c (b ^c (succ k))].
Proof.
move=> aB bB l1b naz.
set (prop:= fun k=> inc k Bnat /\ a <c (b ^c k)).
have pB:(forall x, prop x -> inc x Bnat) by move => k [].
have pz: ~(prop card_zero).
  rewrite /prop cpowx0; move=> [_ a1].
   move: (card_ge1 (CS_Bnat aB) naz)=> h; co_tac.
have exp:(exists x, prop x).
  exists a; split=> //; apply: cpow_M1lt;fprops.
move: (least_int_prop1 pB pz exp)=> [k [kN pks npk]].
ex_tac; last by move: pks => [_ res].
case: (Bnat_to_el (BS_pow bB kN) aB) => //.
by move=>h; case: npk.
Qed.

Definition expansion f b k :=
  [/\ inc b Bnat, inc k Bnat, \1c <c b &
  [/\ fgraph f, domain f = Bint k &
  forall i, inc i (domain f) -> (Vg f i) <c b]].

Definition expansion_value f b :=
  card_sumb (domain f) (fun i=> (Vg f i) *c (b ^c i)).

Section Base_b_expansion.
Variables f g b k k': Set.
Variable Exp: expansion f b k.
Variable Expg: expansion g b (succ k').

Lemma expansion_prop0P i:
   (inc i (domain f)) <-> i <c k.
Proof. move: Exp => [_ kn _ [_ -> _]];exact: (BintP kn). Qed.

Lemma expansion_prop1 i:
  i <c k -> inc (Vg f i) Bnat.
Proof.
move: Exp => [bN kn _ [_ d v]] /expansion_prop0P idf.
move: (v _ idf) => [h _ ]; Bnat_tac.
Qed.

Lemma expansion_prop2:
   finite_int_fam (Lg (domain f) (fun i=> (Vg f i) *c (b ^c i))).
Proof.
move: Exp => [bB kB b2 [fgf df vf]].
hnf; rewrite /allf; bw; split.
  move=> i idf; bw; move /expansion_prop0P: idf => idf.
  apply: (BS_prod (expansion_prop1 idf) (BS_pow bB (BS_lt_int idf kB))).
by rewrite df; apply: finite_Bint.
Qed.

Lemma expansion_prop3: inc (expansion_value f b) Bnat.
Proof.
rewrite /expansion_value; apply: finite_sum_finite.
apply: expansion_prop2.
Qed.

Lemma expansion_prop4: cardinalp k' -> inc k' Bnat.
Proof. move: Expg => [_ kB' _ _] ck; apply: BS_nsucc => //. Qed.

Lemma expansion_prop5: cardinalp k' ->
  expansion (restr g (Bint k')) b k'.
Proof.
move => bk'; move: (expansion_prop4 bk')=> k'n.
move: (Bint_M k'n) => subi.
move: Expg => [bB kB b2 [fgf df vf]].
have dr: (domain (restr g (Bint k')) = Bint k') by bw; ue.
split;fprops; split; fprops.
rewrite dr; move=> i ic; bw; try ue.
by apply: vf; rewrite df; apply: subi.
Qed.

Lemma expansion_prop6: cardinalp k' -> inc (Vg g k') Bnat.
Proof.
move => bk'; move: (expansion_prop4 bk')=> k'n.
move: Expg => [bN kn _ [_ d v]].
have kd: (inc k' (domain g)) by rewrite d; apply:Bint_si.
move: (v _ kd)=> [h _]; Bnat_tac.
Qed.

Lemma expansion_prop7: cardinalp k' ->
  (expansion_value g b) =
   (expansion_value (restr g (Bint k')) b)
   +c (Vg g k' *c (b ^c k')).
Proof.
move => bk'; move: (expansion_prop4 bk')=> k'n.
pose h i := (Vg g i) *c (b ^c i).
have ->: (Vg g k') *c (b ^c k') = h k' by [].
rewrite /expansion_value.
move: (induction_on_sum h k'n); simpl.
have dg: domain g = (Bint (succ k'))
  by move: Expg=> [_ _ _ [_ dg _]].
rewrite -dg; set kk:= (Lg (domain g) h) ; move=> <-.
congr (card_sum _ +c (h k')).
move: (Bint_M k'n) => ii.
have fgg: fgraph g by move : Expg=> [_ _ _ []].
bw;apply: Lg_exten; move=> x xdf /=; bw; ue.
Qed.

End Base_b_expansion.

Lemma expansion_prop8 f b k x:
  let h:= Lg (Bint (succ k)) (fun i=> Yo (i=k) x (Vg f i)) in
 expansion f b k ->
   inc x Bnat -> x <c b ->
    (expansion h b (succ k) /\
      expansion_value h b =
      (expansion_value f b) +c ((b ^c k) *c x)).
Proof.
move=> h Expf xB xb.
move: Expf => [bB kB b2 [fgf df vf]].
have eg: (expansion h b (succ k)).
  red; rewrite /h; bw;split;fprops; split; fprops.
  move=> i idh; bw; Ytac ik => //; apply: vf.
  rewrite df; move: (Bint_pr4 kB)=> [p1 p2].
  move: idh; rewrite - p1; case /setU1_P => //.
have ck: cardinalp k by fprops.
rewrite (expansion_prop7 eg ck).
split; first by exact.
have ->:(restr h (Bint k)= f).
  rewrite /h; symmetry.
  move: (Bint_M kB) => si.
  apply: fgraph_exten=> //.
     fprops.
     bw; fprops.
  rewrite df; move=> y ydf /=; bw; fprops.
  by move: ydf => /(BintP kB) [_ yk]; Ytac0.
have -> //: (Vg h k *c (b ^c k) = (b ^c k) *c x).
by rewrite cprodC /h; bw;[ Ytac0 | apply: (Bint_si kB)].
Qed.

Lemma expansion_prop9 f b k: expansion f b k ->
   (expansion_value f b) <c (b ^c k).
Proof.
move=> Exp.
have kB: inc k Bnat by move: Exp => [bB kB _ _].
move: k kB f Exp.
apply: cardinal_c_induction.
  rewrite cpowx0.
  move=> g [bB _ b2 [fgf df _]].
  rewrite /expansion_value df Bint_co00 /card_sumb csum_trivial.
    apply: card_lt_01.
  bw.
move=> n nB pn g eg.
have cn: (cardinalp n) by fprops.
rewrite (expansion_prop7 eg cn).
move: (expansion_prop5 eg cn) => er.
move: (pn _ er).
move : eg => [bB _ b2 [fgf df vg]].
rewrite pow_succ //.
move: (expansion_prop3 er).
set (a0:= expansion_value (restr g (Bint n)) b).
set (b0:= b ^c n).
have p1: ((Vg g n) <c b).
  by apply: vg; rewrite df; apply:Bint_si.
have cB: inc (Vg g n) Bnat by move: p1 => [aux _]; Bnat_tac.
have b0B: inc b0 Bnat by rewrite /b0; apply: BS_pow.
set c0:= (Vg g n) *c b0.
move => a0B h.
have le1: (a0 +c c0) <c (b0 +c c0).
  apply: csum_Mlteq => //; rewrite /c0; fprops.
suff le2: (b0 +c c0) <=c (b0 *c b) by co_tac.
have cb: cardinalp b0 by fprops.
have ->: b0 +c c0 = b0 *c (succ (Vg g n)).
  rewrite (Bsucc_rw cB) cprod_sumDl (cprod1r cb) cprodC csumC //.
apply: cprod_Mlele; fprops.
by apply /(card_le_succ_ltP _ cB).
Qed.

Lemma expansion_prop10 f b k: cardinalp k ->
  expansion f b (succ k) ->
  card_division_prop (expansion_value f b) (b ^c k) (Vg f k)
  (expansion_value (restr f (Bint k)) b).
Proof.
move=> ck ie.
split.
  rewrite csumC cprodC.
  apply: expansion_prop7 =>//.
apply: expansion_prop9; apply: expansion_prop5 =>//.
Qed.

Lemma expansion_unique f g b k:
  expansion f b k -> expansion g b k ->
  expansion_value f b = expansion_value g b -> f = g.
Proof.
move=> ef eg sm.
have kB: inc k Bnat by move: eg => [_ kB _ _ ].
move: k kB f g sm ef eg.
apply: (cardinal_c_induction).
  rewrite /expansion Bint_co00.
  move=> f1 g1 sv [bB _ _ [fgf df _]] [_ _ _ [fgg dg _]].
  apply: fgraph_exten; [exact | exact | ue | ].
  by rewrite df;move=> x /in_set0.
move=> n nB pn f g sv ef eg.
have cn: cardinalp n by fprops.
move: (expansion_prop10 cn ef) => p1.
move: (expansion_prop10 cn eg) => p2.
rewrite sv in p1.
move: (expansion_prop5 ef cn) => er1.
move: (expansion_prop5 eg cn) => er2.
move:(expansion_prop3 eg) => egB.
have bB: inc b Bnat by move: ef => [bB _].
have cpB: inc (b ^c n) Bnat by fprops.
move: (expansion_prop6 ef cn) => q1B.
move: (expansion_prop6 eg cn) => q2B.
move: (expansion_prop3 er1) => r1B.
move: (expansion_prop3 er2) => r2B.
have bnz: (b ^c n <> card_zero).
  have [_ b0]: (\0c <c b).
    have aux: \0c <=c \1c by fprops.
    move: ef => [_ _ n1b _]; co_tac.
  by apply: cpow_nz => bz; case: b0.
move: (card_division_unique egB cpB q1B r1B q2B r2B bnz p1 p2)=> [pt r].
have aux: (restr f (Bint n) = restr g (Bint n)).
  apply: pn =>//.
move:ef eg=> [_ _ _ [fgf df _]] [_ _ _ [fgg dg _]].
apply: fgraph_exten; [ exact | exact | ue | ].
move=> x xdf.
case: (equal_or_not x n); first by move => ->.
move=> xn.
have xc: (inc x (Bint n)).
  move: xdf; rewrite df;
  move /(BintP(BS_succ nB)) /(card_lt_succ_leP nB) => h.
  by apply /(BintP nB); split.
have <-: (Vg (restr f (Bint n)) x = Vg f x).
  bw; rewrite df; apply: Bint_M =>//.
have <-: (Vg (restr g (Bint n)) x = Vg g x).
  bw; rewrite dg; apply: Bint_M =>//.
ue.
Qed.

Lemma expansion_prop11 f g b k: cardinalp k ->
  expansion f b (succ k) -> expansion g b (succ k) ->
  (Vg f k) <c (Vg g k) ->
  (expansion_value f b) <c (expansion_value g b).
Proof.
move=> ck ef eg ltk.
rewrite (expansion_prop7 ef ck) (expansion_prop7 eg ck).
move: (expansion_prop5 ef ck) => ef1.
move: (expansion_prop5 eg ck) => eg1.
move: (expansion_prop9 ef1).
move: (expansion_prop3 ef1).
move: (expansion_prop3 eg1).
set u:= expansion_value _ _; set v:= expansion_value _ _.
move=> uB vB vp.
move: (expansion_prop4 ef ck) => kB.
move: (expansion_prop6 ef ck) => fB.
move: (expansion_prop6 eg ck) => gB.
set (B:= card_pow b k).
have bB: inc b Bnat by move: ef => [h _].
have BB: (inc B Bnat) by rewrite /B; fprops.
have bb: (B <=c B) by rewrite /B;fprops.
apply: (@card_lt_leT _ (B +c ((Vg f k) *c B))).
  apply: csum_Mlteq; fprops.
apply: (@card_leT _ ((Vg g k) *c B)); last first.
  rewrite csumC; apply: csum_M0le; fprops.
move /(card_le_succ_ltP _ fB): ltk => ltk.
move: (cprod_Mlele ltk bb).
rewrite (Bsucc_rw fB) cprod_sumDr.
by rewrite (cprod1l (CS_Bnat BB)) csumC.
Qed.

Lemma expansion_restr1 f b k l:
  expansion f b k -> l <=c k ->
  expansion (restr f (Bint l)) b l.
Proof.
move=> [bB bK b2 [fgf df vg]] lk.
have lB: inc l Bnat by Bnat_tac.
split; fprops; split; fprops; bw => i idx; bw; apply: vg; rewrite df.
exact: (Bint_M1 bK lk).
Qed.

Lemma expansion_restr2 f b k l:
  expansion f b k -> l <=c k ->
  (forall i, l <=c i -> i <c k -> Vg f i = \0c) ->
  expansion_value (restr f (Bint l)) b = expansion_value f b.
Proof.
move=> ef lk p.
set g := fun i => expansion_value (restr f (Bint i)) b.
have <-: (g k = expansion_value f b).
  move: ef => [bB bK b2 [fgf df vg]].
  rewrite /g -df restr_to_domain //.
set r := fun i=> g l = g i.
change (r k).
have kB: inc k Bnat by move: ef => [bB bK _].
have lB: inc l Bnat by Bnat_tac.
have: inc k (interval_cc Bnat_order l k) by apply/ Bint_ccP1;fprops.
apply: (cardinal_c_induction3_v (r:=r) lB kB); first by trivial.
move=> i /(Bint_coP1 lB kB) [li ik]; rewrite /r => ->.
have iB: inc i Bnat by move: ik => [ik _]; Bnat_tac.
have ci: cardinalp i by fprops.
have ik': (succ i) <=c k by apply /card_le_succ_lt0P; fprops.
move:(expansion_restr1 ef ik').
set F := (restr f (Bint (succ i))).
move=> eF.
rewrite /g (expansion_prop7 eF ci).
set G := (restr F (Bint i)).
have si: sub (Bint (succ i)) (domain f).
  move: ef => [bB bK b2 [fgf df vg]].
  rewrite df; apply: Bint_M1;fprops.
have ->: (restr f (Bint i) = G).
 move: ef => [bB bK b2 [fgf df vg]].
 rewrite /G /F double_restr //.
 apply: Bint_M =>//.
have ->: (Vg F i = card_zero).
  move: ef => [bB bK b2 [fgf df vg]].
  rewrite /F; bw; try apply: p=>//.
  apply:Bint_si =>//.
rewrite cprodC cprod0r csum0r //.
rewrite /expansion_value/card_sumb/card_sum; fprops.
Qed.

Lemma expansion_prop12 f g b kf kg l n:
  n <=c kf -> n <=c kg -> l <c n ->
  (forall i, n <=c i -> i <c kf -> Vg f i = \0c) ->
  (forall i, n <=c i -> i <c kg -> Vg g i = \0c) ->
  (forall i, l <c i -> i <c n -> Vg f i = Vg g i) ->
  expansion f b kf -> expansion g b kg ->
  (Vg f l) <c (Vg g l) ->
  (expansion_value f b) <c (expansion_value g b).
Proof.
move=> nkf nkg ln pf pg pfg ef eg vl.
move: (expansion_restr1 ef nkf).
rewrite -(expansion_restr2 ef nkf pf).
move: (expansion_restr1 eg nkg).
rewrite -(expansion_restr2 eg nkg pg).
set F := (restr f (Bint n)).
set G := (restr g (Bint n)).
move=> eG eF; clear pf pg.
have kfB: inc kf Bnat by move: ef => [_ h _].
have nB: inc n Bnat by Bnat_tac.
have lB: inc l Bnat by move: ln => [ln _]; Bnat_tac.
have pFG: forall i, l <c i -> i <c n -> Vg F i = Vg G i.
  move=> i i1 i2; move: (pfg _ i1 i2).
  have ii: inc i (Bint n) by apply /BintP.
  move: ef eg => [_ _ _ [fgf df vf]] [_ kgB b2 [fgg dg vg]].
  rewrite /F/G; bw.
have vL: (Vg F l) <c (Vg G l).
  have ii: inc l (Bint n) by apply /BintP.
  move: ef eg => [_ _ _ [fgf df vf]] [_ kgB b2 [fgg dg vg]].
  rewrite /F/G; bw.
clear pfg vl ef eg.
set fi := fun i => expansion_value (restr F (Bint i)) b.
set gi := fun i => expansion_value (restr G (Bint i)) b.
have <-: (fi n = expansion_value F b).
  move: eF => [bB bK b2 [fgf df vg]].
  rewrite /fi -df restr_to_domain //.
have <-: (gi n = expansion_value G b).
  move: eG => [bB bK b2 [fgf df vg]].
  rewrite /gi -df restr_to_domain //.
pose r i := (fi i) <c (gi i).
change (r n).
have cl2: inc (succ l) Bnat by fprops.
have cl0: (succ l) <=c n by apply /card_le_succ_ltP.
have rz: (r (succ l)).
  rewrite /r /fi /gi.
  have cl: cardinalp l by fprops.
  have cl1: finite_c l by fprops.
  move: (expansion_restr1 eF cl0) => ef1.
  move: (expansion_restr1 eG cl0) => eg1.
  apply: (expansion_prop11 cl ef1 eg1).
  move: eF eG => [_ _ _ [fgf df vf]] [_ kgB b2 [fgg dg vg]].
  have il: inc l (Bint (succ l)).
    by apply:Bint_si.
  bw.
have: inc n (interval_cc Bnat_order (succ l) n).
   rewrite Bint_ccP1;fprops.
apply: (cardinal_c_induction3_v (r:=r) cl2 nB rz).
clear rz.
move=> i /(Bint_coP1 cl2 nB) [li ik] ri.
have iB: inc i Bnat by move: ik => [ik _]; Bnat_tac.
have ci: cardinalp i by fprops.
have ik': (succ i) <=c n by by apply /card_le_succ_ltP.
move:(expansion_restr1 eF ik').
move:(expansion_restr1 eG ik').
set f1 := (restr F (Bint (succ i))).
set g1 := (restr G (Bint (succ i))).
move=> ef1 eg1; move: ri.
rewrite /r /fi /gi (expansion_prop7 ef1 ci).
rewrite (expansion_prop7 eg1 ci).
set f2 := (restr f1 (Bint i)).
set g2 := (restr g1 (Bint i)).
have si: sub (Bint (succ i)) (domain F).
  move: eF => [bB bK b2 [fgf df vg]].
  rewrite df; apply: Bint_M1; fprops.
have sj: sub (Bint (succ i)) (domain G).
  move: eG => [bB bK b2 [fgf df vg]].
  rewrite df; apply: Bint_M1; fprops.
have ->: (restr F (Bint i) = f2).
  move: eF => [bB bK b2 [fgf df vg]].
  rewrite /f2 /f1 double_restr //.
  apply: Bint_M1; fprops.
have ->: (restr G (Bint i) = g2).
 move: eG => [bB bK b2 [fgf df vg]].
 rewrite /g2 /g1 double_restr //.
 by apply: Bint_M1;fprops.
have ->: (Vg f1 i = Vg g1 i).
  have ii:inc i (Bint (succ i)) by apply:Bint_si.
  move: eF => [bB bK b2 [fgf df vg]].
  move: eG => [_ _ _ [fgf' df' vg']].
  rewrite /f1 /g1; bw; try apply: pFG=>//.
  apply/card_le_succ_lt0P; fprops.
have isi: i <=c (succ i) by fprops.
move:(expansion_restr1 eg1 isi) => ef2.
move:(expansion_restr1 ef1 isi) => eg2.
apply: csum_Mlteq.
  have bB: inc b Bnat by move: ef1 => [ h _].
  apply: BS_prod; fprops.
  apply: (expansion_prop1 ef1); fprops.
apply: (expansion_prop3 eg2).
Qed.

Lemma expansion_prop13 f g b kf kg l:
  kf <=c l -> l <c kg ->
  expansion f b kf -> expansion g b kg ->
  Vg g l <> \0c ->
  (expansion_value f b) <c (expansion_value g b).
Proof.
move=> le1 le2 ef eg vnz.
apply: (@card_lt_leT _ (b ^c kf)).
apply: (expansion_prop9 ef).
move: eg => [bB bK b2 [fgf df vg]].
rewrite /expansion_value /card_sumb.
set F:= Lg _ _.
have fgF: fgraph F by rewrite /F;fprops.
have dF: domain F = Bint kg by rewrite /F -df; bw.
have alc: (forall x, inc x (domain F) -> cardinalp (Vg F x)).
  rewrite dF -df /F => x xdf; bw; fprops.
have ldf: inc l (domain F) by rewrite dF; apply /BintP.
set j:= singleton l.
have sj: sub j (domain F) by move => t /set1_P ->.
move: (csum_increasing1 alc sj).
rewrite (csum_trivial4 _ _ ) (card_card (alc _ ldf)).
suff: (b ^c kf) <=c (Vg F l) by move => p1 p2; co_tac.
have ldg: inc l (domain g) by rewrite df; apply /BintP.
rewrite /F; bw.
have bnz: b<> card_zero by move=>h; rewrite h in b2; case: (card_lt0 b2).
apply: (@card_leT _ (b ^c l)).
  apply: cpow_Mlele; fprops.
rewrite cprodC.
apply: cprod_M1le => //; rewrite /card_pow; fprops.
Qed.

Lemma expansion_prop14 f g b kf kg:
  expansion f b kf -> expansion g b kg ->
  (expansion_value f b) <c (expansion_value g b) ->
  (exists l, [/\ kf <=c l, l <c kg & Vg g l <> \0c])
 \/ (
  exists l n,
  [/\ n <=c kf, n <=c kg, l <c n &
  [/\ (forall i, n <=c i -> i <c kf -> Vg f i = \0c),
  (forall i, n <=c i -> i <c kg -> Vg g i = \0c) ,
  (forall i, l <c i -> i <c n -> Vg f i = Vg g i) &
   (Vg f l) <c (Vg g l)]]).
Proof.
move=> ef eg lt.
have kfb:inc kf Bnat by move: ef => [_ h _].
have kgb:inc kg Bnat by move: eg => [_ h _].
have [n [nf ng nfg]]: exists n,
   [/\ n <=c kf, n <=c kg & (n = kf \/ n = kg)].
  have k1:cardinalp kf by fprops.
  have k2:cardinalp kg by fprops.
  case: (card_le_to_ee k1 k2)=> aux; [exists kf | exists kg];split;fprops.
case: (p_or_not_p (forall i, n <=c i -> i <c kg -> Vg g i = \0c)); last first.
  move=> h.
  have [i [ni ik Vz]]: (exists i, [/\ n <=c i, i <c kg & Vg g i <> \0c]).
   ex_middle h'.
    case: h; move=> i i1 i2.
    case: (p_or_not_p (Vg g i = \0c)) =>// h''; case: h'; exists i => //.
  left; exists i; split => //.
  case: nfg; [by move=> <- | move=> nk; rewrite nk in ni; co_tac ].
move=> pB; right.
case: (p_or_not_p (forall i, n <=c i -> i <c kf -> Vg f i = \0c)); last first.
  move=> h.
  have [i [ni ik Vz]]: (exists i, [/\ n <=c i, i <c kf & Vg f i <> \0c]).
    ex_middle h'; case: h; move=> i i1 i2.
    case: (p_or_not_p (Vg f i = \0c)) =>// h''; case: h'; exists i; split => //.
  have fi: kg <=c i.
  case: nfg; [move=> nk; rewrite nk in ni; co_tac | by move=> <-].
  move: (expansion_prop13 fi ik eg ef Vz) =>[ br _].
  co_tac.
move=> pA.
have nB: inc n Bnat by case: nfg; move=> -> //.
have pC: exists2 l, l <c n& (Vg f l) <> (Vg g l).
  move: (expansion_restr2 ef nf pA) => hf.
  move: (expansion_restr2 eg ng pB) => hg.
  ex_middle bad.
  have eq: (restr f (Bint n) = restr g (Bint n)).
    move: ef eg => [bB bK b2 [fgf df vf]][_ _ _ [fgg dg vg]].
    have s1: sub (Bint n) (domain g).
      rewrite dg; apply: Bint_M1;fprops.
    have s2: sub (Bint n) (domain f).
      rewrite df; apply: Bint_M1;fprops.
    have drf: (domain (restr f (Bint n)) = Bint n) by bw.
    have drg: (domain (restr g (Bint n)) = Bint n) by bw.
    apply: fgraph_exten; fprops.
      ue.
    rewrite drf => x xdf; bw.
    ex_middle nx; case: bad; exists x => //.
    move: xdf => /(BintP nB) => //.
  move: lt;rewrite -hf -hg eq; move => [_ ne]; case: ne; apply: refl_equal.
have [l [lp ln Vl]]: exists l,
    [/\ (forall i : Set, l <c i -> i <c n -> Vg f i = Vg g i),
      l <c n & (Vg f l) <> (Vg g l)].
  set z:= Zo Bnat (fun l => l <c n /\ Vg f l <> Vg g l).
  have nz: nonempty z.
    move: pC => [l lp]; exists l; apply: Zo_i => //.
    move:lp => [lp _];Bnat_tac.
  have pa: (forall a, inc a z -> cardinalp a).
    move=> a /Zo_P [aB _ ]; fprops.
  move: (wordering_cardinal_le_pr pa) => [wor sr].
  move: (worder_total wor) => tor.
  have zc: sub z (Bint n).
    by move=> t /Zo_P [_ [p1 _]]; apply /BintP.
  have fsz: finite_set z.
   by apply: (sub_finite_set zc); apply: finite_Bint.
  have sw: sub z (substrate (graph_on cardinal_le z)) by rewrite sr; fprops.
  move: (finite_subset_torder_greatest tor fsz sw nz)=> [l []].
  move: wor => [or _].
  aw; move=> lz lp; exists l.
  move: (lz); move => /Zo_P [lB [ln Vl]]; split => //.
  move=> i li lin.
  have iB: inc i Bnat by move: lin => [lin _ ]; Bnat_tac.
  case: (equal_or_not (Vg f i) (Vg g i)) => // h.
  have iz: inc i z by apply: Zo_i => //.
  move: (iorder_gle1 (lp _ iz)) => /graph_on_P1 [_ _ il]; co_tac.
exists l; exists n; split => //.
  have p1: cardinalp (Vg f l).
    move: ef =>[bB bK b2 [fgf df vf]].
    have ldf: (inc l (domain f)) by rewrite df; apply /BintP => //; co_tac.
    by move: (vf _ ldf)=> [[res _] _ ].
  have p2: cardinalp (Vg g l).
    move: eg =>[bB bK b2 [fgf df vf]].
    have ldf: (inc l (domain g)) by rewrite df;apply /BintP => //; co_tac.
    by move: (vf _ ldf)=> [[res _] _ ].
  case: (card_le_to_el p2 p1) => //.
  move=> h.
  have p3: (Vg g l) <c (Vg f l) by split => //; apply: nesym.
  have lp' : forall i, l <c i -> i <c n -> Vg g i = Vg f i.
    by move=> i i1 i2; symmetry;move: (lp _ i1 i2).
  move: (expansion_prop12 ng nf ln pB pA lp' eg ef p3) => [p4 _].
  co_tac.
Qed.

Lemma expansion_exists1 a b k:
  inc b Bnat -> \1c <c b -> inc k Bnat ->
  inc a Bnat -> a <c (b ^c k) ->
  exists2 f, expansion f b k & expansion_value f b = a.
Proof.
move=> bB b1 kB; move: k kB a.
apply: cardinal_c_induction.
  rewrite cpowx0 => c cB c1.
  exists (Lg emptyset (fun _ => card_zero)) => //;bw.
    split;fprops; split; fprops.
      by bw; rewrite - Bint_co00.
    by bw; move=> i /in_set0.
  rewrite /expansion_value/card_sumb; bw; rewrite csum_trivial; bw.
  move: c1; rewrite - succ_zero; move / (card_lt_succ_leP BS0) => aux.
  by symmetry; apply: card_le0.
move=> n nB pn c cB cp.
set (b0:= b ^c n).
have b0B: (inc b0 Bnat) by rewrite /b0; fprops.
have Bz: (b0 <> card_zero).
  have aux:(\0c <c b) by move: card_lt_01 => aux'; co_tac.
  have bnz: b<> card_zero by move: aux => [_]; apply: nesym.
  apply: (cpow_nz bnz).
move: (card_division_exists cB b0B Bz) => [q [r [qB rB [aux lt]]]].
rewrite /b0 in lt.
move: (pn _ rB lt) => [f ise ev].
have p1: (b0 *c q) <c (b0 *c b).
  have p2: ((b0 *c q) <=c c).
    rewrite aux; apply: csum_M0le; fprops.
  have p3: (inc (b0 *c q) Bnat) by fprops.
  rewrite /b0 - pow_succ -/b0; fprops.
  co_tac.
move: (cprod_lt_simplifiable b0B qB bB Bz p1) => qb.
move: (expansion_prop8 ise qB qb).
set F:= (Lg _ _).
move=> [s1 s2]; exists F => //.
rewrite s2 ev aux csumC /b0; apply: refl_equal.
Qed.

Lemma expansion_exists a b: inc a Bnat -> inc b Bnat ->
  \1c <c b -> exists k f,
    (expansion f b k /\ expansion_value f b = a).
Proof.
move=> aB bB b1; exists a.
have [f pa pb]:exists2 f, expansion f b a & expansion_value f b = a.
  by apply: expansion_exists1 => //; apply: cpow_M1lt; fprops.
by exists f.
Qed.

Definition eqmod a b B:= a %%c B = b %%c B.

Section ModuloProps.
Variable B: Set.
Hypothesis Bn: inc B Bnat.
Hypothesis Bnz: B <> \0c.

Lemma crem_prop a b: inc a Bnat -> inc b Bnat ->
  eqmod ((B *c a) +c b) b B.
Proof.
move=> aB bB; rewrite /eqmod.
move: (card_division bB Bn Bnz).
set q := b %/c B; set r := b %%c B.
move=> [q1B r1B [aeq r1p]].
rewrite aeq csumA - cprod_sumDl.
set q2:= (a +c q).
have q2B: inc q2 Bnat by rewrite /q2; apply: BS_sum.
set A:= ((B *c q2) +cr).
have dp: (card_division_prop A B q2 r) by split;[apply: refl_equal | done].
move: (cquorem_pr (BS_sum (BS_prod Bn q2B) r1B) Bn q2B r1B dp).
by move=> [_ h]; symmetry.
Qed.

Lemma crem_sum a b: inc a Bnat -> inc b Bnat ->
  eqmod (a +c b) ((a %%c B) +c (b %%c B)) B.
Proof.
move=> aB bB.
move: (card_division aB Bn Bnz) (card_division bB Bn Bnz).
rewrite /card_division_prop.
set q1:= a %/cB; set q2:= b %/c B; set r1:= a %%c B; set r2:= b %%c B.
move=> [q1B r1B [aeq r1p]][q2B r2B [beq r2p]].
rewrite aeq beq.
set t := _ +c _.
have ->: t= (B *c (q1 +c q2)) +c (r1 +c r2).
  rewrite cprod_sumDl csumA.
  set (s1:= B *c q1); set (s2:= B *c q2).
  by rewrite /t (csum_permute24) -/s1 -/s2 csumA.
apply:(crem_prop (BS_sum q1B q2B) (BS_sum r1B r2B)).
Qed.

Lemma crem_mult a b: inc a Bnat -> inc b Bnat ->
  eqmod (a *c b) ((a %%c B) *c (b %%c B)) B.
Proof.
move=> aB bB.
move: (card_division aB Bn Bnz<