Library sset10b

Theory of Sets EIII-6 Infinite sets

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

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Import ssrint.
Require Export sset10.

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

Module RationalIntegers.

The set of rational integers

Z is the disjoint union of N* and N; J x C1 is positive, J y C0 is negative

Ltac qprops := auto with qprops.
Ltac qw := autorewrite with qw.

We define 0 and the injections N -> Zp and N -> Zm

Definition BZ_of_nat x := J x C1.

We define 0 1 2 3 4 and -1 as elements of Z

Definition BZ_zero := BZ_of_nat \0c.
Definition BZ_one := BZ_of_nat \1c.
Definition BZ_two := BZ_of_nat \2c.
Definition BZ_three := BZ_of_nat \3c.
Definition BZ_four := BZ_of_nat \4c.

Notation "\0z" := BZ_zero.
Notation "\1z" := BZ_one.
Notation "\2z" := BZ_two.
Notation "\3z" := BZ_three.
Notation "\4z" := BZ_four.

Definition BZm_of_nat x := Yo (x = \0c) \0z (J x C0).
Definition BZ_mone := BZm_of_nat \1c.
Notation "\1mz" := BZ_mone.

We define Z Zp Zm Zps Zms and Ns (p=positive, m=negative s = nonzero)

Definition Bnats:= Bnat -s1 \0c.
Definition BZ := canonical_du2 Bnats Bnat.
Definition BZms:= Bnats *s1 C0.
Definition BZp:= Bnat *s1 C1.
Definition BZps:= Bnats *s1 C1.
Definition BZm:= BZms +s1 \0z.

We show that some sets are subsets of others

Lemma sub_BZp_BZ : sub BZp BZ.
Proof.
by move => t /indexed_P [pa pb pc]; rewrite - pa pc; apply :candu2_prb.
Qed.

Lemma sub_BZps_BZp : sub BZps BZp.
Proof.
by move => t /indexed_P [pa] /setC1_P [pb pc] pd; apply indexed_P.
Qed.

Lemma sub_BZps_BZ : sub BZps BZ.
Proof. apply: (sub_trans sub_BZps_BZp sub_BZp_BZ). Qed.

Lemma sub_BZms_BZm : sub BZms BZm.
Proof. by move => t ts; apply /setU1_P; left. Qed.

Lemma sub_BZms_BZ : sub BZms BZ.
Proof.
by move => t /indexed_P [pa pb pc]; rewrite - pa pc; apply :candu2_pra.
Qed.

Lemma sub_BZm_BZ : sub BZm BZ.
Proof.
move => t; case /setU1_P; first by apply: sub_BZms_BZ.
by move => ->; apply :candu2_prb; fprops.
Qed.

Hint Resolve sub_BZm_BZ sub_BZms_BZ sub_BZp_BZ sub_BZps_BZ : qprops.
Hint Resolve sub_BZms_BZm sub_BZps_BZp : qprops.

We show that the injections have values in Zp and Zm

Lemma BZ_of_natp_i x: inc x Bnat -> inc (BZ_of_nat x) BZp.
Proof. by move => xb; apply: indexed_pi. Qed.

Lemma BZ_of_nat_i x: inc x Bnat -> inc (BZ_of_nat x) BZ.
Proof. by move => xb;apply:sub_BZp_BZ;apply:BZ_of_natp_i. Qed.

Lemma BZm_of_natms_i x: inc x Bnat -> x <> \0c ->
  inc (BZm_of_nat x) BZms.
Proof.
by move => xB xnz;rewrite /BZm_of_nat; Ytac0; apply: indexed_pi;apply /setC1_P.
Qed.

Lemma BZm_of_natm_i x: inc x Bnat -> inc (BZm_of_nat x) BZm.
Proof.
move => xb; rewrite /BZm_of_nat; Ytac xnz; first by apply /setU1_P; right.
by apply /setU1_P; left; apply: indexed_pi; apply /setC1_P.
Qed.

Lemma BZm_of_nat_i x: inc x Bnat -> inc (BZm_of_nat x) BZ.
Proof. move => h; move: (BZm_of_natm_i h); qprops.
Qed.

Lemma BZ0_pr1: P \0z = \0c.
Proof. rewrite /BZ_zero /BZ_of_nat;aw. Qed.

Lemma BZ0_pr2: Q \0z = C1.
Proof. rewrite /BZ_zero /BZ_of_nat;aw. Qed.

Hint Rewrite BZ0_pr1 BZ0_pr2: qw.

Lemma BZps_pr1nz x: inc x BZps -> P x <> \0c.
Proof. by move /indexed_P => [_] /setC1_P [_]. Qed.

Lemma BZps_iP x: inc x BZps <-> (inc x BZp /\ x <> \0z).
Proof.
split.
  move => /indexed_P [pa ] /setC1_P [pb pc] pd;split => //.
    by apply /indexed_P.
  by dneg pe; rewrite pe; qw.
move => [] /indexed_P [pa pb pc] pd; apply /indexed_P;split => //.
apply /setC1_P;split => //.
dneg pe;rewrite /BZ_zero /BZ_of_nat; apply: pair_exten;aw;fprops.
Qed.

Lemma BZms_nz x: inc x BZms -> x <> \0z.
Proof. move => /indexed_P [_ _ h2] h; move: h2;rewrite h BZ0_pr2; fprops. Qed.

Lemma BZps_nz x: inc x BZps -> x <> \0z.
Proof. by move /BZps_iP => []. Qed.

Lemma BZms_iP x: inc x BZms <-> (inc x BZm /\ x <> \0z).
Proof.
split; last by move => [] /setU1_P; case.
by move => h; move: (BZms_nz h)=> xnz;split => //; apply /setU1_P;left.
Qed.

We show that N -> Zp and N -> Zm are injective

Lemma BZ_of_nat_pr1 x: P (BZ_of_nat x) = x.
Proof. rewrite /BZ_of_nat; aw. Qed.

Lemma BZm_of_nat_pr1 x: P (BZm_of_nat x) = x.
Proof. by rewrite /BZm_of_nat; Ytac xz; aw; rewrite BZ0_pr1 xz. Qed.

Lemma BZ_of_nat_inj x y: BZ_of_nat x = BZ_of_nat y -> x = y.
Proof. by move => h; move: (f_equal P h); rewrite ! BZ_of_nat_pr1. Qed.

Lemma BZm_of_nat_inj x y: BZm_of_nat x = BZm_of_nat y -> x = y.
Proof. by move => h; move: (f_equal P h); rewrite ! BZm_of_nat_pr1. Qed.

Lemma BZm_of_nat_inj_bis x y: BZm_of_nat x = BZ_of_nat y -> (x = y /\ x = \0c).
Proof.
rewrite / BZm_of_nat; Ytac xz.
   by move => h; move: (f_equal P h);rewrite xz /BZ_zero /BZ_of_nat;aw.
by move => h; move: (f_equal Q h); rewrite /BZ_of_nat;aw => bad; case: TP_ne.
Qed.

Lemma BZ_0_if_abs0 x: inc x BZ -> P x = \0c -> x = \0z.
Proof.
move /candu2P => [pa]; case; first by move => [] /setC1_P [].
move => [_ pb] pc; rewrite/BZ_zero /BZ_of_nat; apply: pair_exten;aw; fprops.
Qed.

We show that 0, 1, etc are rational integers
Lemma BZS0 : inc \0z BZ.
Proof. apply:BZ_of_nat_i; fprops. Qed.

Lemma BZpS0 : inc \0z BZp.
Proof. apply: indexed_pi; fprops. Qed.

Lemma BZmS0 : inc \0z BZm.
Proof. by apply /setU1_P; right. Qed.

Lemma BZS1 : inc \1z BZ.
Proof. apply:BZ_of_nat_i; fprops. Qed.

Lemma BZps1 : inc \1z BZps.
Proof. apply: indexed_pi; apply /setC1_P;split;fprops. Qed.

Lemma BZS2 : inc \2z BZ.
Proof. apply:BZ_of_nat_i; fprops. Qed.

Lemma BZS3 : inc \3z BZ.
Proof. apply:BZ_of_nat_i; apply: BS3. Qed.

Lemma BZS4 : inc \4z BZ.
Proof. apply:BZ_of_nat_i; apply: BS4. Qed.

Lemma BZSm1 : inc \1mz BZ.
Proof. apply:BZm_of_nat_i; fprops. Qed.

Lemma BZmsS_m1: inc \1mz BZms.
Proof. apply:BZm_of_natms_i; fprops. Qed.

Hint Resolve BZS0 BZS1 BZSm1: qprops.
Lemma BZ_one_not_zero: \1z <> \0z.
Proof.
rewrite /BZ_one /BZ_zero /BZ_of_nat =>h; move: (f_equal P h);aw; fprops.
Qed.

Lemma BZ_mone_not_zero: \1mz <> \0z.
Proof.
rewrite /BZ_mone /BZm_of_nat; Ytac k; first by case: card1_nz.
move => h; move: (f_equal P h);aw; rewrite BZ0_pr1; fprops.
Qed.

More properties of integers

Lemma BZ_pr1 a: inc a BZ -> inc (P a) Bnat.
Proof. by move /candu2P => [_]; case => [] [] // /setC1_P []. Qed.

Lemma BZ_pr2 x: inc x BZ -> (Q x = C0 \/ Q x = C1).
Proof. apply: candu2_pr2. Qed.

Lemma BZp_pr2 x: inc x BZp -> Q x = C1.
Proof. by move /indexed_P => [_]. Qed.

Lemma BZps_pr2 x: inc x BZps -> Q x = C1.
Proof. by move /indexed_P => [_]. Qed.

Lemma BZms_pr2 x: inc x BZms -> Q x = C0.
Proof. by move /indexed_P => [_]. Qed.

Lemma BZms_hi_pr x: inc x BZms -> (P x <> \0c /\ BZm_of_nat (P x) = x).
Proof.
move /indexed_P => [pa] /setC1_P [pb pc] pd;split => //.
by rewrite /BZm_of_nat; Ytac0; rewrite - {2} pa pd.
Qed.

Lemma BZp_hi_pr x: inc x BZp -> BZ_of_nat (P x) = x.
Proof. by move /indexed_P => [pa pb pc]; rewrite /BZ_of_nat -{2} pa pc. Qed.

Lemma BZm_hi_pr x: inc x BZm -> BZm_of_nat (P x) = x.
Proof.
rewrite /BZm_of_nat;case /setU1_P.
  by move /indexed_P => [pa] /setC1_P [pb pc] pd; Ytac0; rewrite -{2} pa pd.
by move => ->; rewrite BZ0_pr1; Ytac0.
Qed.

Lemma BZ_hi_pr a: inc a BZ -> a = BZ_of_nat (P a) \/ a = BZm_of_nat (P a).
Proof.
move /candu2P => [pa]; case => [] [pb pc].
  right; symmetry; apply:BZm_hi_pr; apply /setU1_P; left.
  by apply/ indexed_P.
by left; symmetry; apply BZp_hi_pr; apply/ indexed_P.
Qed.

We have a partition of Z as Zp and Zms, but there are more such partitions


Lemma BZ_i0P x: inc x BZ <-> (inc x BZms \/ inc x BZp).
Proof.
split; last by case => h; qprops.
move /candu2P => [pa] [] [pb pc].
  by left; rewrite -pa pc; apply: indexed_pi.
by right; rewrite -pa pc; apply: indexed_pi.
Qed.

Lemma BZ_i1P x: inc x BZ <-> [\/ x = \0z, inc x BZps | inc x BZms].
Proof.
split.
   move /BZ_i0P; case => h; first by constructor 3.
   case: (equal_or_not x \0z); first by constructor 1.
   by constructor 2; apply /BZps_iP.
case; first move => ->; qprops.
Qed.

Lemma BZ_i2P x: inc x BZ <-> (inc x BZps \/ inc x BZm).
Proof.
split; last by case => xs; qprops.
case /BZ_i1P; [by move => ->; right; apply /setU1_P;right | by left | right ].
by apply /setU1_P;left.
Qed.

Lemma BZ_di_neg_pos x: inc x BZms -> inc x BZp -> False.
Proof. move => h1 h2; move : (BZms_pr2 h1); rewrite (BZp_pr2 h2); fprops. Qed.

Lemma BZ_di_pos_neg x: inc x BZps -> inc x BZm -> False.
Proof.
move /BZps_iP=> [p1 p2]; case /setU1_P => // p3; apply: (BZ_di_neg_pos p3 p1).
Qed.

Lemma BZ_di_neg_spos x: inc x BZms -> inc x BZps -> False.
Proof.
move => h; move:(sub_BZms_BZm h) =>h1 h2; apply:BZ_di_pos_neg h2 h1.
Qed.

Lemma BZp_i a : inc a BZ -> Q a = C1 -> inc a BZp.
Proof.
by move => az ap; case /BZ_i0P: az => // h; case: TP_ne;rewrite - (BZms_pr2 h).
Qed.

Lemma BZms_i a : inc a BZ -> Q a = C0 -> inc a BZms.
Proof.
by move => az ap; case /BZ_i0P: az => // h; case: TP_ne;rewrite - (BZp_pr2 h).
Qed.

We show that Ns and Z are infinite countable

Lemma equipotent_Bnats_Bnat: Bnats \Eq Bnat.
Proof.
apply /card_eqP; symmetry;apply cardinal_setC1_inf; apply: infinite_Bnat.
Qed.

Lemma infinite_countable_Z: BZ \Eq Bnat.
Proof.
apply /card_eqP.
have ->: cardinal BZ = Bnats +c Bnat by [].
have ->: Bnats +c Bnat = cardinal Bnat +c cardinal Bnat.
  apply: csum2_pr4; fprops; eqtrans Bnat; apply: equipotent_Bnats_Bnat.
apply:sum2_infinite1; apply /infinite_setP; apply: infinite_Bnat.
Qed.

Opposite

The oppositive of a number is obtained by swapping C0 and C1 in the second component, except for zero

Definition BZopp x:= Yo (Q x = C0) (BZ_of_nat (P x))(BZm_of_nat (P x)).

Definition BZopp_fun := Lf BZopp BZ BZ.

Lemma BZSo x: inc x BZ -> inc (BZopp x) BZ.
Proof.
move => xz; move: (BZ_pr1 xz) => pB.
rewrite /BZopp; Ytac aux; [ by apply:BZ_of_nat_i | by apply:BZm_of_nat_i ].
Qed.

Lemma BZopp_0 : BZopp \0z = \0z.
Proof.
rewrite /BZopp {1} /BZ_zero /BZ_of_nat; aw; Ytac0.
by rewrite BZ0_pr1 / BZm_of_nat; Ytac0.
Qed.

Hint Rewrite BZopp_0: qw.
Hint Resolve BZSo : qprops.

Oppositive maps Zp to Zm and Zps to Zms. It is an involution of Z

Lemma BZopp_pr1 x: P (BZopp x) = P x.
Proof.
rewrite /BZopp; Ytac sx; first by rewrite BZ_of_nat_pr1.
by rewrite BZm_of_nat_pr1.
Qed.

Lemma BZnon_zero_opp x: inc x BZ -> (x <> \0z <-> BZopp x <> \0z).
Proof.
move => xz; split => h ha; case: h; last by rewrite ha; qw.
by apply: (BZ_0_if_abs0 xz); rewrite - (BZopp_pr1 x) ha; qw.
Qed.

Lemma BZopp_pr2 x: inc x BZ -> x <> \0z ->
   ((Q x = C0 -> Q (BZopp x) = C1)
     /\ (Q x = C1 -> Q (BZopp x) = C0)).
Proof.
move => pa pb.
have pnz: (P x <> \0c) by move => h; case: pb; apply: BZ_0_if_abs0.
by rewrite /BZopp /BZ_of_nat /BZm_of_nat; Ytac0;Ytac sx; aw; rewrite ? sx.
Qed.

Lemma BZopp_positive1 x: inc x BZps -> inc (BZopp x) BZms.
Proof.
move /BZps_iP => [pa pb]; move: (BZp_pr2 pa)(sub_BZp_BZ pa) => h1 h2.
apply: (BZms_i (BZSo h2)) (proj2 (BZopp_pr2 h2 pb) h1).
Qed.

Lemma BZopp_positive2 x: inc x BZp -> inc (BZopp x) BZm.
Proof.
case:(equal_or_not x \0z); first by move => -> _; rewrite BZopp_0; apply:BZmS0.
by move => pa pb;apply /setU1_P; left; apply BZopp_positive1; apply /BZps_iP.
Qed.

Lemma BZopp_negative1 x: inc x BZms -> inc (BZopp x) BZps.
Proof.
move => xn; move : (sub_BZms_BZ xn) => xz.
move: (BZms_nz xn) => xnz ;apply/ BZps_iP; split.
  exact: (BZp_i (BZSo xz) (proj1 (BZopp_pr2 xz xnz) (BZms_pr2 xn))).
by apply /(BZnon_zero_opp xz).
Qed.

Lemma BZopp_negative2 x: inc x BZm -> inc (BZopp x) BZp.
Proof.
case /setU1_P => h; first by move: (BZopp_negative1 h) => /BZps_iP [].
by rewrite h BZopp_0; apply: BZpS0.
Qed.

Lemma BZopp_K x: inc x BZ -> BZopp (BZopp x) = x.
Proof.
move => xz.
move: TP_ne => ns.
rewrite {1} /BZopp BZopp_pr1 /BZopp; case: (equal_or_not(Q x) C0) => h; Ytac0.
  rewrite /BZ_of_nat; aw; Ytac0;apply:BZm_hi_pr.
  move/candu2P: xz => [px]; case; last by move => [_]; rewrite h.
  move => [pa pb];apply /setU1_P;left;apply /indexed_P;split => //.
rewrite /BZm_of_nat; case: (equal_or_not (P x) \0c) => h1; Ytac0.
  by rewrite BZ0_pr2; Ytac0; symmetry;apply: BZ_0_if_abs0.
aw; Ytac0;apply:BZp_hi_pr; move/candu2P: xz => [px]; case; first by move => [_].
by move => [pa pb]; apply /indexed_P.
Qed.

Lemma BZopp_inj a b: inc a BZ -> inc b BZ -> BZopp a = BZopp b -> a = b.
Proof.
by move => az bz h;rewrite - (BZopp_K az) h (BZopp_K bz).
Qed.

Lemma BZopp_fb: bijection BZopp_fun.
Proof.
apply: lf_bijective.
- move => t tz; qprops.
- apply: BZopp_inj.
- move => y yz; exists (BZopp y) => //;qprops; symmetry; by apply BZopp_K.
Qed.

Lemma BZopp_p x: BZopp (BZ_of_nat x) = BZm_of_nat x.
Proof. by rewrite /BZopp /BZ_of_nat; aw; Ytac0. Qed.

Lemma BZopp_m x: BZopp (BZm_of_nat x) = BZ_of_nat x.
Proof.
rewrite /BZm_of_nat; Ytac bz; first by rewrite BZopp_0 bz.
by rewrite /BZopp; aw; Ytac0.
Qed.

Lemma BZopp_m1: BZopp \1mz = \1z.
Proof. by rewrite /BZ_mone BZopp_m. Qed.

Lemma BZopp_1: BZopp \1z = \1mz.
Proof. by rewrite /BZ_one BZopp_p. Qed.

Hint Resolve BZmsS_m1:qprops.

Absolute value

Absolute value is the number with a positive sign; and same numeric value

Definition BZabs x := BZ_of_nat (P x).

Lemma BZabs_pos: forall x, inc x BZp -> BZabs x = x.
Proof. move => xz; apply:BZp_hi_pr. Qed.

Lemma BZabs_neg x: inc x BZms -> BZabs x = BZopp x.
Proof. by move => xz; rewrite /BZabs /BZopp (BZms_pr2 xz); Ytac0. Qed.

Lemma BZabs_m1: BZabs \1mz = \1z.
Proof. by rewrite (BZabs_neg BZmsS_m1) BZopp_m1. Qed.

Lemma BZabs_1: BZabs \1z = \1z.
Proof. exact (BZabs_pos(sub_BZps_BZp BZps1)). Qed.

Lemma BZabs_iN x: inc x BZ -> inc (BZabs x) BZp.
Proof. by move => h;rewrite /BZabs; apply: BZ_of_natp_i; apply: BZ_pr1. Qed.

Lemma BZSa x: inc x BZ -> inc (BZabs x) BZ.
Proof. by move => h; apply:sub_BZp_BZ; apply:BZabs_iN. Qed.

Lemma BZabs_pr1 x: P (BZabs x) = P x.
Proof. rewrite /BZabs /BZ_of_nat; aw. Qed.

Lemma BZabs_pr2 x: inc x BZ -> Q (BZabs x) = C1.
Proof. rewrite /BZabs /BZ_of_nat; aw. Qed.

Lemma BZabs_abs x: BZabs (BZabs x) = BZabs x.
Proof. by rewrite /BZabs BZabs_pr1. Qed.

Lemma BZabs_opp x: BZabs (BZopp x) = BZabs x.
Proof. by rewrite /BZabs BZopp_pr1. Qed.

Lemma BZabs_0 : BZabs \0z = \0z.
Proof. by rewrite /BZabs BZ0_pr1. Qed.

Hint Rewrite BZabs_0: qw.

Lemma BZabs_0p x: inc x BZ -> BZabs x = \0z -> x = \0z.
Proof.
move => pa pb; move: (f_equal P pb); rewrite BZabs_pr1 BZ0_pr1.
apply: (BZ_0_if_abs0 pa).
Qed.

Hint Resolve BZSa: qprops.

Ordering on Z

We use the ordinal sum of the opposite ordering of Ns and N. This is clearly a total ordering

Definition BZ_ordering:=
  order_sum2 (opp_order (induced_order Bnat_order Bnats)) Bnat_order.

Lemma BZ_order_aux1: sub Bnats (substrate Bnat_order).
Proof. by rewrite (proj2 Bnat_order_wor) => t /setC1_P []. Qed.

Lemma BZ_order_aux:
  order (opp_order (induced_order Bnat_order Bnats))
  /\ order Bnat_order.
Proof.
move: Bnat_order_wor => [[or _] _]; move: BZ_order_aux1 => h.
move: (proj1 (iorder_osr or h)) => h1; move: (proj1 (opp_osr h1)) => h2.
split;fprops.
Qed.

Lemma BZor_or: order BZ_ordering.
Proof. by move: BZ_order_aux => [pa pb]; apply: orsum2_or. Qed.

Lemma BZor_sr: substrate BZ_ordering = BZ.
Proof.
move: Bnat_order_wor => [[or _] sr]; move: BZ_order_aux1 => s1.
move: (proj1 (iorder_osr or s1)) => h1; move: (opp_osr h1) => [h2 h3].
rewrite orsum2_sr // h3 sr; aw.
Qed.

Lemma BZor_tor: total_order BZ_ordering.
Proof.
move:BZ_order_aux1 => h1.
move: (worder_total (proj1 Bnat_order_wor)) => h2.
apply:orsum2_totalorder => //.
by apply:total_order_opposite; apply:total_order_sub.
Qed.

Definition BZ_le x y:= [/\ inc x BZ, inc y BZ &
  [\/ [/\ Q x = C0, Q y = C0 & (P y) <=c (P x)],
      [/\ Q x = C0 & Q y = C1] |
      [/\ Q x = C1, Q y = C1 & (P x) <=c (P y)]]].
Definition BZ_lt x y:= BZ_le x y /\ x <> y.

Notation "x <=z y" := (BZ_le x y) (at level 60).
Notation "x <z y" := (BZ_lt x y) (at level 60).

We define le, lt, ge and gt on Z, and state properties of this operation

Lemma BZ_le_P x y: gle BZ_ordering x y <-> x <=z y.
Proof.
apply: (iff_trans (orsum2_gleP _ _ x y)).
move: BZ_order_aux => [pa pb].
move: BZor_sr; rewrite orsum2_sr //; move => ->.
split.
  have hh: forall z, inc z BZ -> Q z = C0 \/ Q z = C1.
    move => z /candu2P [_]; case; move => [_ ->]; fprops.
  move => [ra rb rc]; split => //; case: rc.
      move => [rd re] /opp_gleP => h; constructor 1;split => //.
      by move: (iorder_gle1 h) => /Bnat_order_leP [_ _].
    move => [rd re] /Bnat_order_leP [_ _ rf]; constructor 3;split => //.
     case: (hh _ ra) => //.
    case: (hh _ rb) => //.
  by move => [rd re]; constructor 2;split => //;case: (hh _ rb) => qv.
move => [ra rb rc];split => //.
move /candu2P: ra => [_ ra]; move /candu2P: rb => [_ rb].
case: rc.
    move => [rd re rf]; constructor 1 ;split => //.
    case: ra; [move => [p1 _] | by move => [_]; rewrite rd =>h; case: TP_ne].
    case: rb; [move => [p2 _] | by move => [_]; rewrite re =>h; case: TP_ne ].
    apply /opp_gleP; apply /iorder_gleP => //.
    apply /Bnat_order_leP; split => //.
      by case /setC1_P: p2 => [].
    by case /setC1_P: p1.
  by move => [rd re]; constructor 3;split => //; rewrite re=>h; case: TP_ne.
move => [rd re rf]; constructor 2;split => //.
    rewrite rd; fprops.
  rewrite re; fprops.
case: ra; [ by move => [_]; rewrite rd => h; case: TP_ne | move => [p1 _] ].
case: rb; [ by move => [_]; rewrite re => h; case: TP_ne | move => [p2 _] ].
by apply /Bnat_order_leP.
Qed.

Lemma BZ_leT a b c: a <=z b -> b <=z c -> a <=z c.
Proof.
move: BZor_or => h /BZ_le_P pa /BZ_le_P pb; apply /BZ_le_P;order_tac.
Qed.

Lemma BZ_leR a: inc a BZ -> a <=z a.
Proof.
by move: BZor_or => h az;apply /BZ_le_P; order_tac;rewrite BZor_sr.
Qed.

Lemma BZ_leA a b: a <=z b -> b <=z a -> a = b.
Proof. move: BZor_or => h /BZ_le_P pa /BZ_le_P pb; order_tac. Qed.

Lemma BZ_le_lt_not a b: a <=z b -> b <z a -> False.
Proof. by move => pa [pb]; case; apply:BZ_leA. Qed.

Lemma BZ_lt_leT a b c: a <z b -> b <=z c -> a <z c.
Proof.
move => [pa pb] pc;split; first apply: (BZ_leT pa pc).
move => ac; case: pb. apply :BZ_leA => //; ue.
Qed.

Lemma BZ_le_ltT a b c: a <=z b -> b <z c -> a <z c.
Proof.
move => pa [pb pc];split; first apply: (BZ_leT pa pb).
move => ac; case: pc;apply :BZ_leA => //; ue.
Qed.

Ltac BZo_tac := match goal with
  | Ha: ?a <=z ?b, Hb: ?b <=z ?c |- ?a <=z ?c
     => apply: (BZ_leT Ha Hb)
  | Ha: ?a <z ?b, Hb: ?b <=z ?c |- ?a <z ?c
     => apply: (BZ_lt_leT Ha Hb)
  | Ha:?a <=z ?b, Hb: ?b <z ?c |- ?a <z ?c
     => apply: (BZ_le_ltT Ha Hb)
  | Ha: ?a <z ?b, Hb: ?b <z ?c |- ?a <z ?c
     => induction Ha; BZo_tac
  | Ha: ?a <=z ?b, Hb: ?b <z ?a |- _
    => case: (BZ_le_lt_not Ha Hb)
  | Ha: ?x <=z ?y, Hb: ?y <=z ?x |- _
   => solve [ rewrite (BZ_leA Ha Hb) ; fprops ]
  | Ha: inc ?x BZ |- ?x <=z ?x => apply: (BZ_leR Ha)
  | Ha: ?a <=z _ |- inc ?a BZ => exact (proj31 Ha)
  | Ha: _ <=z ?a |- inc ?a BZ => exact (proj32 Ha)
  | Ha: ?a <z _ |- inc ?a BZ => exact (proj31_1 Ha)
  | Ha: _ <z ?a |- inc ?a BZ => exact (proj32_1 Ha)
  | Ha: ?a <z ?b |- ?a <=c ?b => by move: Ha => []
end.

Lemma BZ_le_to_ee a b: inc a BZ -> inc b BZ -> a <=z b \/ b <=z a.
Proof.
move: BZor_tor => [_]; rewrite BZor_sr => h pa pb.
by case: (h _ _ pa pb)=> h1; [left | right]; apply /BZ_le_P.
Qed.

Lemma BZ_le_to_ell a b: inc a BZ -> inc b BZ -> [\/ a = b, a <z b | b <z a].
Proof.
move => pa pb; case: (equal_or_not a b); first by constructor 1.
by move => na; case: (BZ_le_to_ee pa pb)=> h1; [constructor 2 | constructor 3];
   split => //; apply: nesym.
Qed.

Lemma BZ_le_to_el a b: inc a BZ -> inc b BZ -> a <=z b \/ b <z a.
Proof.
move=> ca cb; case: (BZ_le_to_ell ca cb).
- by move=> ->; left; BZo_tac.
- by move => [pa _]; left.
- by right.
Qed.

Lemma BZ_le_P1 x y: inc x BZp -> inc y BZp ->
  ( x <=z y <-> (P x) <=c (P y)).
Proof.
move => pa pb; move: (BZp_pr2 pa) (BZp_pr2 pb) => pc pd.
split.
  move => [_ _]; rewrite pc; by case; move => [ba] => //; case: TP_ne.
move => h; split => //; qprops; constructor 3 => //.
Qed.

Lemma BZ_le_pr2 x y: inc x BZp -> inc y BZms -> y <z x.
Proof.
move => pa pb; move:(BZp_pr2 pa) (BZms_pr2 pb) => pc pd.
split; first by split => //; qprops; constructor 2.
move => xy; move: (f_equal Q xy); rewrite pc pd; fprops.
Qed.

Lemma BZ_le_P3 x y: inc x BZms -> inc y BZms ->
  (x <=z y <-> (P y) <=c (P x)).
Proof.
move => pa pb; move: (BZms_pr2 pa) (BZms_pr2 pb) => pc pd.
split.
  by move => [_ _]; rewrite pd; case => [][aa bb] //; case: TP_ne.
move => h; split => //; qprops; constructor 1 => //;apply: sub_BZms_BZ.
Qed.

Lemma BZ_le_pr4 x y: inc x BZp -> inc y BZms -> ~ ( x <=z y).
Proof. move => pa pb; move: (BZ_le_pr2 pa pb) => pc pd; BZo_tac. Qed.

Lemma BZ_le_P0 x y:
   x <=z y <->
   [\/ [/\ inc x BZms, inc y BZms & (P y) <=c (P x)],
       [/\ inc x BZms & inc y BZp] |
       [/\ inc x BZp, inc y BZp & (P x) <=c (P y)]].
Proof.
split.
  move => h; move:(h) => [pa pb _].
  case /BZ_i0P: pa => ha; case /BZ_i0P: pb => hb.
  by constructor 1 ;split => //; move /(BZ_le_P3 ha hb): h.
  by constructor 2; split => //.
  by move: (BZ_le_pr4 ha hb) => hc.
  by constructor 3;split => //; move /(BZ_le_P1 ha hb): h.
case; first by move => [pa pb pc]; apply /BZ_le_P3.
  by move => [pa pb]; exact: (proj1 (BZ_le_pr2 pb pa)).
by move => [pa pb pc]; apply /BZ_le_P1.
Qed.

Lemma BZ_le_pr5 x y: inc x BZp -> inc y BZp ->
  (x <=z y = (BZabs x) <=z (BZabs y)).
Proof. move => pa pb; rewrite !BZabs_pos //. Qed.

Lemma BZ_lt_P1 x y: inc x BZp -> inc y BZp ->
  (x <z y <-> (P x) <c (P y)).
Proof.
move => pa pb; split.
  move => [] /(BZ_le_P1 pa pb) => pc pd;split => //.
  by move => sp; case: pd; rewrite - (BZp_hi_pr pa) - (BZp_hi_pr pb) sp.
move => [pc pd]; split; first by apply /(BZ_le_P1 pa pb).
by move => xy; move: (f_equal P xy).
Qed.

Lemma BZ_positive_P x: \0z <=z x <-> inc x BZp.
Proof.
split.
  move => [pa pb pc]; case /BZ_i0P: pb => // xn.
  move: (BZms_pr2 xn) => qx.
  by move: pc;rewrite BZ0_pr2 qx; case;move => [ta tb] => //;case: TP_ne.
move => xp; split => //;qprops; rewrite BZ0_pr2 BZ0_pr1; constructor 3.
rewrite (BZp_pr2 xp);split => //; move: (BZ_pr1 (sub_BZp_BZ xp)) => t; fprops.
Qed.

Lemma BZ_positive_P1 x: \0z <z x <-> inc x BZps.
Proof.
split.
   move => [] /BZ_positive_P pa pb; apply /BZps_iP;split;fprops.
by move /BZps_iP => [pa pb]; split; [apply /BZ_positive_P |apply: nesym].
Qed.

Lemma BZ_negative_P x: x <z \0z <-> inc x BZms.
Proof.
split.
  move => pa; case /BZ_i0P: (proj31_1 pa) => //.
  move /BZ_positive_P => h; BZo_tac.
move => h; move: (BZ_le_to_el BZS0 (sub_BZms_BZ h)); case => //.
move /BZ_positive_P => h1;case:(BZ_di_neg_pos h h1).
Qed.

Lemma BZ_negative_P1 x: x <=z \0z <-> inc x BZm.
Proof.
split.
   move => h; apply /setU1_P;case: (equal_or_not x \0z) => xnz; first by right.
   by left; apply /BZ_negative_P; split.
case /setU1_P; first by move /BZ_negative_P => [].
move => ->;move: BZS0 => h; BZo_tac.
Qed.

Lemma BZ_le_P6 x y: inc x BZm -> inc y BZm ->
  (x <=z y <-> (P y) <=c (P x)).
Proof.
case /setU1_P => xnz; case /setU1_P => ynz.
- apply /(BZ_le_P3 xnz ynz).
- rewrite ynz BZ0_pr1; split.
    move => _; move: (BZ_pr1 (sub_BZms_BZ xnz)) => xn; fprops.
    by move /BZ_negative_P: xnz => [pa _ ] _.
- rewrite xnz; split.
    by move/BZ_positive_P => h; case:(BZ_di_neg_pos ynz h).
  rewrite BZ0_pr1 => pc; move /indexed_P: ynz => [_] /setC1_P [pa pb] _.
  case: pb; exact (card_le0 pc).
- rewrite xnz ynz BZ0_pr1;move :BZS0 =>h; split=> _; fprops; BZo_tac.
Qed.

Lemma BZabs_positive b: inc b BZ -> b <> \0z -> \0z <z (BZabs b).
Proof.
move => pa pb; apply /BZ_positive_P1.
apply /BZps_iP;split; first by apply BZabs_iN.
by move => h; case: pb; apply:BZabs_0p.
Qed.

Opposite is an order isomorphism from (Z,<) to (Z,>)

Lemma BZ_le_opp x y: x <=z y -> (BZopp y) <=z (BZopp x).
Proof.
move => leq; move: (leq) => [xz yz etc].
case: (equal_or_not x \0z) => xnz.
   move: leq; rewrite xnz => /BZ_positive_P yp; rewrite BZopp_0.
   by apply/BZ_negative_P1; apply: BZopp_positive2.
case: (equal_or_not y \0z) => ynz.
   move: leq; rewrite ynz => /BZ_negative_P1 yp;rewrite BZopp_0.
   by apply/BZ_positive_P; apply: BZopp_negative2.
split => //; qprops; rewrite (BZopp_pr1 x) (BZopp_pr1 y).
move: (BZopp_pr2 xz xnz) (BZopp_pr2 yz ynz) => [qa qb][qc qd].
case: etc.
- by move => [pa pb pc]; rewrite (qa pa) (qc pb); constructor 3.
- by move => [pa pb]; rewrite (qa pa) (qd pb); constructor 2.
- by move => [pa pb pc]; rewrite (qb pa) (qd pb); constructor 1.
Qed.

Lemma BZ_le_opp_iso:
  order_isomorphism BZopp_fun BZ_ordering (opp_order BZ_ordering).
Proof.
move: BZor_or BZor_sr BZopp_fb => or sr bf.
have la: lf_axiom BZopp BZ BZ by move => t tz; qprops.
move: (opp_osr or) => [pa pb].
red;rewrite pb /BZopp_fun; aw;split => //.
  fprops.
  split; aw=> //.
hnf; aw;move => x y xz yz; aw;split.
  by move /BZ_le_P => h; apply /opp_gleP; apply /BZ_le_P;apply BZ_le_opp.
move /opp_gleP /BZ_le_P => h; apply /BZ_le_P.
by rewrite - (BZopp_K xz) -(BZopp_K yz); apply BZ_le_opp.
Qed.

Lemma BZ_lt_opp x y: x <z y -> (BZopp y) <z (BZopp x).
Proof.
move => [pa pb]; split; first by apply:BZ_le_opp.
by move: pa => [xz yz _] pc; case: pb; apply:BZopp_inj.
Qed.

Lemma BZ_lt_oppP x y: inc x BZ -> inc y BZ ->
  (x <z y <-> (BZopp y) <z (BZopp x)).
Proof.
move => pa pb; split; first by apply: BZ_lt_opp.
by move=> h; move: (BZ_lt_opp h); rewrite (BZopp_K pa) (BZopp_K pb).
Qed.

Addition


Definition BZsum x y:=
  let abs_sum := (P x) +c (P y) in
    let abs_diff1 := (P x) -c (P y) in
      let abs_diff2 := (P y) -c (P x) in
        Yo (inc x BZp /\ inc y BZp) (BZ_of_nat abs_sum)
        (Yo ( ~ inc x BZp /\ ~ inc y BZp) (BZm_of_nat abs_sum)
          (Yo (inc x BZp /\ ~ inc y BZp)
            (Yo ( (P y) <=c (P x))
              (BZ_of_nat abs_diff1) (BZm_of_nat abs_diff2))
            (Yo ( (P x) <=c (P y))
              (BZ_of_nat abs_diff2) (BZm_of_nat abs_diff1)))).

Notation "x +z y" := (BZsum x y) (at level 50).

Lemma BZsumC x y: x +z y = y +z x.
Proof.
rewrite /BZsum.
case: (p_or_not_p (inc y BZp /\ inc x BZp)) => h.
  have h': (inc x BZp /\ inc y BZp) by apply /Logic.and_comm.
  by Ytac0; Ytac0; rewrite csumC.
have h': not (inc x BZp /\ inc y BZp) by apply /Logic.and_comm.
Ytac0; Ytac0.
case: (p_or_not_p (~ inc y BZp /\ ~ inc x BZp)) => h2.
  have h2': (~ inc x BZp /\ ~ inc y BZp) by apply /Logic.and_comm.
  by Ytac0; Ytac0; rewrite csumC.
have h2': ~ (~ inc x BZp /\ ~ inc y BZp) by apply /Logic.and_comm.
Ytac0; Ytac0.
case: (p_or_not_p (inc y BZp /\ ~ inc x BZp)) => h3.
  have h3': ~(inc x BZp /\ ~ inc y BZp) by move => [pa pb]; case: h3.
  by Ytac0; Ytac0.
have h3': (inc x BZp /\ ~ inc y BZp).
  split; first by ex_middle bad; case: h3; split => //; ex_middle bad2; case:h2.
  by move => bad; case:h3; split => //; move => h4; case: h.
by Ytac0; Ytac0.
Qed.

Lemma BZsum_pp x y: inc x BZp -> inc y BZp ->
  x +z y = BZ_of_nat ((P x) +c (P y)).
Proof. move => xp yp;rewrite /BZsum Y_true //;split => //. Qed.

Lemma BZsum_mm x y: inc x BZms -> inc y BZms ->
  x +z y = BZm_of_nat ( (P x) +c (P y)).
Proof.
move => xm ym.
have pa: (~ inc x BZp) by move => pa; case: (BZ_di_neg_pos xm pa).
have pb: (~ inc y BZp) by move => pb; case: (BZ_di_neg_pos ym pb).
have pc: ~(inc x BZp /\ inc y BZp) by case.
by rewrite /BZsum; Ytac0; rewrite (Y_true (conj pa pb)).
Qed.

Lemma BZsum_pm x y: inc x BZp -> inc y BZms ->
  x +z y = (Yo ((P y) <=c (P x))
    (BZ_of_nat ((P x) -c (P y)))
    (BZm_of_nat ((P y) -c(P x)))).
Proof.
move => xp ym.
have pb: (~ inc y BZp) by move => pb; case: (BZ_di_neg_pos ym pb).
have pa: ~(inc x BZp /\ inc y BZp) by case.
have pc: ~(~ inc x BZp /\ ~ inc y BZp) by case.
move: (conj xp pb) => pd.
by rewrite /BZsum; Ytac0; Ytac0; Ytac0.
Qed.

Lemma BZsum_pm1 x y: inc x BZp -> inc y BZms ->
  (P y) <=c (P x) -> x +z y = BZ_of_nat((P x) -c (P y)).
Proof. by move => pa pb pc; rewrite BZsum_pm //; Ytac0. Qed.

Lemma BZsum_pm2 x y: inc x BZp -> inc y BZms ->
  (P x) <c (P y) -> x +z y = (BZm_of_nat ((P y) -c (P x))).
Proof.
move => pa pb pc; rewrite BZsum_pm // Y_false //.
move => h;apply: (not_card_le_lt h pc).
Qed.

Lemma BZSs x y: inc x BZ -> inc y BZ -> inc (x +z y) BZ.
Proof.
move => xz yz; rewrite /BZsum.
move: (BZ_pr1 xz)(BZ_pr1 yz) => pxn qxn.
Ytac h1; first apply:BZ_of_nat_i; fprops.
Ytac h2; first apply:BZm_of_nat_i; fprops.
Ytac h3; first by
   Ytac h4; [apply:BZ_of_nat_i; fprops | apply:BZm_of_nat_i; fprops].
Ytac h4; [apply:BZ_of_nat_i; fprops | apply:BZm_of_nat_i; fprops].
Qed.

Hint Resolve BZSs: qprops.

Lemma BZsum_0l x: inc x BZ -> \0z +z x = x.
Proof.
move => xz; rewrite /BZsum BZ0_pr1; move: BZpS0 (BZ_pr1 xz) => z0 Px.
case: (p_or_not_p (inc x BZp)) => xp.
  by rewrite (Y_true (conj z0 xp)) (bsum0l Px) (BZp_hi_pr xp).
have h1: ~(inc \0z BZp /\ inc x BZp) by case.
have h2: ~ (~ inc \0z BZp /\ ~ inc x BZp) by case.
move: (conj z0 xp) => h3.
Ytac0; Ytac0; Ytac0;case /BZ_i0P: xz => // xms.
move: (sub_BZms_BZm xms) => xm.
move /indexed_P: xms => [_] /setC1_P [_] h _.
Ytac h4; first by case: h; apply:card_le0.
by rewrite (cdiff_n_0 Px) (BZm_hi_pr xm).
Qed.

Lemma BZsum_0r x: inc x BZ -> x +z \0z = x.
Proof. by move => xz;rewrite BZsumC BZsum_0l. Qed.

Hint Rewrite BZsum_0l BZsum_0r: qw.

Lemma BZsum_opp_r x: inc x BZ -> x +z (BZopp x) = \0z.
Proof.
have aux: (forall y, inc y BZps ->y +z (BZopp y) = \0z).
  move => y yp; move: (BZopp_positive1 yp) => yp1.
  move: (sub_BZps_BZp yp) => yp2.
  case: (inc_or_not (BZopp y) BZp) => h1; first by case: (BZ_di_neg_pos yp1 h1).
  have h2: ~(inc y BZp /\ inc (BZopp y) BZp) by case.
  have h3:~(~ inc y BZp /\ ~ inc (BZopp y) BZp) by case.
  rewrite /BZsum; Ytac0; Ytac0.
  rewrite (Y_true (conj yp2 h1)) /BZopp (BZps_pr2 yp); Ytac0.
  rewrite /BZm_of_nat (Y_false (BZps_pr1nz yp)); aw.
  by rewrite cdiff_n_n; Ytac h4 => //; Ytac0.
case /BZ_i1P; first by move => ->; qw => //; qprops.
  by apply: aux.
move => xm; move: (BZopp_negative1 xm) => xm1.
by rewrite BZsumC - {2} (BZopp_K (sub_BZms_BZ xm)); apply: aux.
Qed.

Lemma BZsum_opp_l x: inc x BZ -> (BZopp x) +z x = \0z.
Proof. by move => h; rewrite BZsumC BZsum_opp_r. Qed.

Hint Rewrite BZsum_opp_l BZsum_opp_r: qw.

Lemma BZsum_opp_distr x y: inc x BZ -> inc y BZ ->
  BZopp (x +z y) = (BZopp x) +z (BZopp y).
Proof.
pose R a b := BZopp (a +z b) = BZopp a +z BZopp b.
have ha :forall a b, inc a BZps -> inc b BZms -> R a b.
  move => a b ap bn; rewrite /R.
  move: (sub_BZps_BZp ap) => ap1.
  rewrite (BZsum_pm ap1 bn).
  move: (BZ_pr1 (sub_BZps_BZ ap)) (BZ_pr1 (sub_BZms_BZ bn)) => pa pb.
  case: (equal_or_not (P a) (P b)) => pab.
    have hb: (BZopp b = a).
      by rewrite /BZopp -pab (BZms_pr2 bn); Ytac0; apply BZp_hi_pr.
    rewrite hb (BZsum_opp_l (sub_BZps_BZ ap)).
    rewrite Y_true pab; [ by rewrite cdiff_n_n -/BZ_zero; qw | fprops].
  move: (BZopp_positive1 ap) (BZopp_negative1 bn) => nab nbc.
  rewrite BZsumC (BZsum_pm (sub_BZps_BZp nbc) nab) ! BZopp_pr1.
  case: (card_le_to_ee (CS_Bnat pb) (CS_Bnat pa)) => h.
    have h1: ~(P a <=c P b) by move => h2; case: pab; co_tac.
    by Ytac0; Ytac0; rewrite /BZ_of_nat /BZopp; aw; Ytac0.
  have h1: ~(P b <=c P a) by move => h2; case: pab; co_tac.
  move: (cdiff_nz (conj h pab)) => h2.
  by rewrite /BZopp /BZm_of_nat; Ytac0; Ytac0; Ytac0;aw; Ytac0; Ytac0.
have hb :forall a b, inc a BZps -> inc b BZps -> R a b.
  move => a b pa pb.
  move: (BZopp_positive1 pa) (BZopp_positive1 pb) => n1 n2.
  rewrite /R BZsum_pp; qprops; rewrite BZsum_mm; qprops; rewrite ! BZopp_pr1.
  by rewrite /BZopp /BZ_of_nat; aw; Ytac0.
have hc :forall a b, inc a BZps -> inc b BZ -> R a b.
  move => a b az bz; case /BZ_i1P: bz.
    move: (sub_BZps_BZ az) => az1; move => ->; rewrite /R;qw => //; qprops.
    by move=> bz; apply: hb.
  by move=> bz;apply: ha.
move => xz yz; case /BZ_i1P: (xz) => xs.
   rewrite xs /R;qw => //; qprops.
  by apply: hc.
symmetry;rewrite - {2} (BZopp_K yz) - {2} (BZopp_K xz).
move: (BZopp_negative1 xs) (BZSo xz) (BZSo yz) => xz1 xz2 yz1.
rewrite - (hc _ _ xz1 yz1) BZopp_K //; qprops.
Qed.

Lemma BZsum_N_Ns x y: inc x Bnat -> inc y Bnats -> inc (x +c y) Bnats.
Proof.
move => xb /setC1_P [yn yz]; apply /setC1_P;split => //;fprops.
move: (cpred_pr yn yz) => [pa pb].
rewrite pb (csum_via_succ _ pa);apply: succ_nz.
Qed.

Lemma BZpS_sum x y: inc x BZp -> inc y BZp -> inc (x +z y) BZp.
Proof.
move => pa pb; rewrite (BZsum_pp pa pb); apply BZ_of_natp_i.
move: (BZ_pr1 (sub_BZp_BZ pa)) (BZ_pr1 (sub_BZp_BZ pb)) => sa sb; fprops.
Qed.

Lemma BZpsS_sum_r x y: inc x BZp -> inc y BZps -> inc (x +z y) BZps.
Proof.
move => pa pb.
move: (pa) (pb) => /indexed_P [_ q1 _] /indexed_P [_ q2 _].
move /BZps_iP: pb => [pb pc];rewrite (BZsum_pp pa pb); apply /indexed_pi.
apply: (BZsum_N_Ns q1 q2).
Qed.

Lemma BZpsS_sum_l x y: inc x BZps -> inc y BZp -> inc (x +z y) BZps.
Proof. by move => pa pb; rewrite BZsumC; apply BZpsS_sum_r. Qed.

Lemma BZpsS_sum_rl x y: inc x BZps -> inc y BZps -> inc (x +z y) BZps.
Proof. by move => pa pb; apply: BZpsS_sum_r => //;apply:sub_BZps_BZp. Qed.

Lemma BZmsS_sum_rl x y: inc x BZms -> inc y BZms -> inc (x +z y) BZms.
Proof.
move => xz yz.
move: (BZopp_negative1 xz) (BZopp_negative1 yz) => xz1 yz1.
move: (sub_BZms_BZ xz)(sub_BZms_BZ yz) => xz2 yz2.
move:( BZpsS_sum_rl xz1 yz1); rewrite - (BZsum_opp_distr xz2 yz2) => h.
by move: (BZopp_K (BZSs xz2 yz2)) => <-; apply: BZopp_positive1.
Qed.

Lemma BZmsS_sum_r x y: inc x BZm -> inc y BZms -> inc (x +z y) BZms.
Proof.
case /setU1_P; first by apply:BZmsS_sum_rl.
move => -> h; qw; qprops.
Qed.

Lemma BZmsS_sum_l x y: inc x BZms -> inc y BZm -> inc (x +z y) BZms.
Proof. by move => pa pb;rewrite BZsumC; apply: BZmsS_sum_r. Qed.

Lemma BZmS_sum x y: inc x BZm -> inc y BZm -> inc (x +z y) BZm.
Proof.
case /setU1_P; first by move => pa pb; apply:sub_BZms_BZm; apply:BZmsS_sum_l.
move => -> h; qw; qprops.
Qed.

Lemma BZsumA x y z: inc x BZ -> inc y BZ -> inc z BZ ->
  x +z (y +z z) = (x +z y) +z z.
Proof.
move: x y z.
pose f x := Yo (inc x BZp) (J \0c (P x)) (J (P x) \0c).
pose g x := Yo ((P x) <=c (Q x))
    (BZ_of_nat((Q x) -c (P x))) (BZm_of_nat ((P x) -c (Q x))).
have Ha: forall x, inc x BZ -> g (f x) = x.
   move => x xz; rewrite /f/g; case: (inc_or_not x BZp) => h1; Ytac0; aw.
     move: (BZ_pr1 xz) => pa; move: (czero_least (CS_Bnat pa)) => h2; Ytac0.
     by rewrite (cdiff_n_0 pa); apply: BZp_hi_pr.
   case /BZ_i0P: xz => zt; last by [].
   move /indexed_P: (zt) => [_] /setC1_P [pa pb] _.
   have hh: ~(P x <=c \0c).
     move => h; move /(strict_pos_P pa): (nesym pb) => h2; co_tac.
   Ytac0 ;rewrite (cdiff_n_0 pa); apply: BZm_hi_pr; qprops.
set (NN:= Bnat \times Bnat).
pose h x y := J ( (P x) +c (P y)) ( (Q x) +c (Q y)).
have Hu: forall x y, inc x NN -> inc y NN
    -> ((g x = g y) <-> ( (P x) +c (Q y) = (P y) +c (Q x))).
  move => x y /setX_P [_ pa pb] /setX_P [_ pc pd]; rewrite /g.
  case:(card_le_to_el (CS_Bnat pa)(CS_Bnat pb)) => h1;
     case:(card_le_to_el (CS_Bnat pc)(CS_Bnat pd)) => h2.
  - Ytac0; Ytac0; move: (cdiff_pr h1) (cdiff_pr h2).
    set a:= Q x -c P x; set b:= Q y -c P y; move => eqa eqb.
    rewrite /BZ_of_nat; split => ha.
      by rewrite - eqa -eqb (pr1_def ha) csumA (csumA (P y)) (csumC (P y)).
    congr (J _ C1); move: ha; rewrite -eqa csumA - eqb csumA (csumC (P x)).
    move => t; symmetry;apply:(csum_simplifiable_left (BS_sum pc pa) _ _ t);
    rewrite /a /b; fprops.
  - have h3: ~(P y <=c Q y) by move => h3; co_tac.
    move: (cdiff_nz h2) => h4.
    Ytac0; Ytac0; rewrite /BZ_of_nat /BZm_of_nat; Ytac0; split => h5.
      by case: TP_ne1; move: (pr2_def h5).
    by move: (csum_Mlelt pb pc h1 h2); rewrite h5 csumC; move => [_].
  - have h3: ~(P x <=c Q x) by move => h3; co_tac.
    move: (cdiff_nz h1) => h4.
    Ytac0; Ytac0; rewrite /BZ_of_nat /BZm_of_nat; Ytac0; split => h5.
      by case: TP_ne1; move: (pr2_def h5).
    by move: (csum_Mlelt pd pa h2 h1); rewrite - h5 csumC; move => [_].
  - have h3: ~(P x <=c Q x) by move => h3; co_tac.
    have h4: ~(P y <=c Q y) by move => h4; co_tac.
    move: (cdiff_nz h2) => h5.
    move: (cdiff_nz h1) => h6.
    Ytac0; Ytac0; rewrite /BZm_of_nat; Ytac0; Ytac0.
    move: (cdiff_pr(proj1 h1)) (cdiff_pr (proj1 h2)).
    set a:= P x -c Q x; set b:= P y -c Q y; move => eqa eqb.
    split => ha.
      by rewrite - eqa -eqb (pr1_def ha) - csumA csumC (csumC b).
    congr (J _ C0); move: ha; rewrite -eqa csumC csumA - eqb.
    rewrite (csumC _ b) - (csumA b) (csumC (Q y)) (csumC b) => t.
    apply:(csum_simplifiable_left (BS_sum pb pd) _ _ t); rewrite /a /b; fprops.
have Hb: forall x y, inc x BZp -> inc y BZms -> x +z y = g (h (f x) (f y)).
  move => x y xp ym ; rewrite /f.
  have yp: ~(inc y BZp) by move => bad; case: (BZ_di_neg_pos ym bad).
  move: (CS_Bnat(BZ_pr1 (sub_BZp_BZ xp))) => cx.
  move: (CS_Bnat(BZ_pr1 (sub_BZms_BZ ym))) => cy.
  Ytac0; Ytac0; rewrite /h /g !pr1_pair !pr2_pair; aw.
  case: (card_le_to_el cy cx) => cxy.
    by rewrite (BZsum_pm1 xp ym cxy); Ytac0.
  Ytac aux; [ by co_tac | by rewrite (BZsum_pm2 xp ym cxy) ].
have H: (forall x y, inc x BZ -> inc y BZ -> x +z y = g (h (f x) (f y))).
  have Hc : forall x y, inc x BZp -> inc y BZ -> x +z y = g (h (f x) (f y)).
    move => x y xp; case /BZ_i0P; first by apply: Hb.
    move => yp; rewrite /f/h/g; Ytac0; Ytac0; aw; last by apply: CS0.
    move: (BZ_pr1 (sub_BZp_BZ xp)) (BZ_pr1 (sub_BZp_BZ yp)) => pa pb.
    move: (BS_sum pa pb) => sB; move: (czero_least (CS_Bnat sB)) => pc; Ytac0.
    rewrite (cdiff_n_0 sB); apply (BZsum_pp xp yp).
  move => x y xz yz; case /BZ_i0P: (xz) => pa; last by apply: Hc.
  have aux: (h (f x) (f y) = h (f y) (f x)).
    by rewrite /h csumC (csumC (Q (f x))).
  case /BZ_i0P: (yz) => pb; last by rewrite aux BZsumC; apply: Hc.
  have qa: ~(inc x BZp) by move => qa; case: (BZ_di_neg_pos pa qa).
  have qb: ~(inc y BZp) by move => qb; case: (BZ_di_neg_pos pb qb).
  rewrite /f; Ytac0; Ytac0;rewrite /g/h; aw; last by apply: CS0.
  move: (BZ_pr1 (sub_BZms_BZ pa)) (BZ_pr1 (sub_BZms_BZ pb)) => pc pd.
  move: (BS_sum pc pd) => sB; rewrite (cdiff_n_0 sB).
  Ytac aa; last by apply (BZsum_mm pa pb).
  move /indexed_P: pb => [_ ha _].
  move: (BZsum_N_Ns pc ha) => /setC1_P [_]; case; apply: (card_le0 aa).
have Hf:forall x, inc x BZ -> inc (f x) NN.
  move => x xz; move: (BZ_pr1 xz) => pb.
  rewrite /f; Ytac t; apply: setXp_i; fprops.
have Hg:forall x, inc x NN -> inc (g x) BZ.
  move => x /setX_P [_ pa pb]; rewrite /g; Ytac aux.
    by apply: BZ_of_nat_i; apply:BS_diff.
    by apply: BZm_of_nat_i; apply:BS_diff.
have Hh:forall u v, inc u NN -> inc v NN -> inc (h u v) NN.
  move => u v /setX_P [_ pa pb] /setX_P [_ pc pd]; apply: setXp_i; fprops.
move => x y z xZ yZ zZ; move: (BZSs xZ yZ) (BZSs yZ zZ).
set (yz:= y +z z); set (xy:= x +z y) => xyZ yzZ.
have : (g (f yz) = g (h (f y) (f z))) by rewrite Ha // /yz - (H _ _ yZ zZ).
move /(Hu _ _ (Hf _ yzZ) (Hh _ _ (Hf _ yZ) (Hf _ zZ))) => eq1.
have: (g (f xy) = g (h (f x) (f y))) by rewrite Ha // /xy - (H _ _ xZ yZ).
move /(Hu _ _ (Hf _ xyZ) (Hh _ _ (Hf _ xZ) (Hf _ yZ))) => eq2.
rewrite (H _ _ xZ yzZ) (H _ _ xyZ zZ).
apply /(Hu _ _ (Hh _ _ (Hf _ xZ) (Hf _ yzZ)) (Hh _ _ (Hf _ xyZ) (Hf _ zZ))).
move: eq1 eq2;rewrite /h !pr1_pair !pr2_pair.
move: (Hf _ xZ) => /setX_P [_].
move: (Hf _ yZ) => /setX_P [_ ].
move: (Hf _ zZ) => /setX_P [_].
move: (Hf _ xyZ) => /setX_P [_ ].
move: (Hf _ yzZ) => /setX_P [_].
set (Px:= P (f x)); set (Qx:=Q (f x)); set (Py:= P (f y)); set (Qy:=Q (f y)).
set (Pz:= P (f z)); set (Qz:=Q (f z)); set (Pyz:= P (f yz)).
set (Qyz:= Q (f yz)) ; set (Pxy:= P (f xy)); set (Qxy:= Q (f xy)).
move => pyzb qyzb pxyb qxyb pzb qzb pyb qyb pxb qxb eq1 eq2.
apply: (csum_simplifiable_right qyb); [ fprops | fprops |].
rewrite - csumA - csumA.
set a := Pyz +c _.
have -> : a = (Pyz +c (Qy +c Qz)) +c Qxy.
  rewrite /a - (csumA _ _ Qxy); congr (Pyz +c _).
  by rewrite csumC (csumC Qxy) csumA.
set b := _ +c Qy.
have -> : b = ((Pxy +c (Qx +c Qy)) +c Qyz) +c Pz.
  rewrite /b - !csumA; congr (Pxy +c _).
  by rewrite csumC - !csumA (csumA Qyz Qy Pz) (csumC Qyz Qy) (csumA Qy Qyz Pz).
rewrite eq1 eq2 - !csumA; congr (Px +c _); congr (Py +c _).
by rewrite csumC (csumC _ Qxy) csumA.
Qed.

Lemma BZsum_permute_2_in_4 a b c d:
  inc a BZ -> inc b BZ -> inc c BZ -> inc d BZ ->
  (a +z b) +z (c +z d) = (a +z c) +z (b +z d).
Proof.
move => az bz cz dz.
rewrite (BZsumA (BZSs az bz) cz dz) (BZsumC a) - (BZsumA bz az cz).
by rewrite (BZsumA (BZSs az cz) bz dz) (BZsumC b).
Qed.

Multiplication


Definition BZprod x y :=
  let aux := BZ_of_nat ((P x) *c (P y)) in
     (Yo (Q x = Q y) aux (BZopp aux)).

Notation "x *z y" := (BZprod x y) (at level 40).

Definition BZprod_sign_aux x y:=
  Yo (x = \0z) C1 (Yo (y= \0z) C1 (Yo (Q x = Q y) C1 C0)).

Lemma BZprodC x y: x *z y = y *z x.
Proof.
rewrite /BZprod cprodC.
case: (equal_or_not (Q x) (Q y)); first by move => ->.
by move => h; move: (nesym h) => h1; Ytac0; Ytac0.
Qed.

Lemma BZprod_0r x: x *z \0z = \0z.
Proof. by rewrite /BZprod BZ0_pr1 cprod0r -/BZ_zero; qw; Ytac xx. Qed.

Lemma BZprod_0l x: \0z *z x = \0z.
Proof. by rewrite BZprodC BZprod_0r. Qed.

Hint Rewrite BZprod_0l BZprod_0r: qw.

Lemma BZprod_abs2 x y: inc x BZ -> inc y BZ ->
  x *z y = J ((P x) *c (P y)) (BZprod_sign_aux x y).
Proof.
move => xz yz; rewrite /BZprod_sign_aux.
case: (equal_or_not x \0z).
   by move => ->; qw; rewrite cprodC cprod0r; Ytac0.
move=> xnz;case: (equal_or_not y \0z).
   by move => ->; qw; rewrite cprod0r; Ytac0; Ytac0.
move => ynz; Ytac0; Ytac0.
rewrite /BZprod; Ytac qxy; Ytac0 => //; rewrite /BZopp /BZ_of_nat; aw; Ytac0.
rewrite /BZm_of_nat Y_false //; apply cprod2_nz.
  move => pz; case: xnz; apply: (BZ_0_if_abs0 xz pz).
move => pz; case: ynz; apply: (BZ_0_if_abs0 yz pz).
Qed.

Lemma BZprod_pr1 x y: P (x *z y) = (P x) *c (P y).
Proof. by rewrite /BZprod; Ytac aux; rewrite ?BZopp_pr1 BZ_of_nat_pr1. Qed.

Lemma BZprod_aux x y: inc x BZ -> inc y BZ -> inc ((P x) *c (P y)) Bnat.
Proof. move => pa pb;move: (BZ_pr1 pa)(BZ_pr1 pb) => pc pd; fprops. Qed.

Lemma BZSp x y: inc x BZ -> inc y BZ -> inc (x *z y) BZ.
Proof.
move => pa pb; move: (BZ_of_nat_i (BZprod_aux pa pb)) => h.
rewrite /BZprod; Ytac h1 => //; qprops.
Qed.

Hint Resolve BZSp: qprops.

Lemma BZprod_pp x y: inc x BZp -> inc y BZp ->
    x *z y = BZ_of_nat ((P x) *c (P y)).
Proof. by move => pa pb; rewrite /BZprod (BZp_pr2 pa)(BZp_pr2 pb); Ytac0. Qed.

Lemma BZprod_mm x y: inc x BZms -> inc y BZms->
    x *z y = BZ_of_nat ((P x) *c (P y)).
Proof. by move => pa pb; rewrite /BZprod (BZms_pr2 pa)(BZms_pr2 pb); Ytac0. Qed.

Lemma BZprod_pm x y: inc x BZp -> inc y BZms->
   x *z y = BZm_of_nat ((P x) *c (P y)).
Proof.
move => pa pb; rewrite /BZprod (BZp_pr2 pa)(BZms_pr2 pb).
Ytac0;rewrite /BZopp /BZ_of_nat pr2_pair; Ytac0; aw.
Qed.

Lemma BZprod_mp x y: inc x BZms -> inc y BZp ->
  x *z y = BZm_of_nat ((P x) *c (P y)).
Proof. by move => pa pb; rewrite BZprodC;rewrite BZprod_pm // cprodC. Qed.

Lemma BZprod_nz x y: inc x BZ -> inc y BZ ->
  x <> \0z -> y <> \0z -> x *z y <> \0z.
Proof.
move => xz yz xnz ynz zz.
move: (f_equal P zz); rewrite BZprod_pr1 BZ0_pr1; apply: cprod2_nz.
  move => pz; case: xnz; apply: (BZ_0_if_abs0 xz pz).
move => pz; case: ynz; apply: (BZ_0_if_abs0 yz pz).
Qed.

Lemma BZprod_abs x y: inc x BZ -> inc y BZ ->
  BZabs (x *z y) = (BZabs x) *z (BZabs y).
Proof.
move => pa pb;symmetry.
by rewrite (BZprod_pp (BZabs_iN pa) (BZabs_iN pb)) !BZabs_pr1 /BZabs BZprod_pr1.
Qed.

Lemma BZprod_1l x: inc x BZ -> \1z *z x = x.
Proof.
move => xz; move: (CS_Bnat (BZ_pr1 xz)) => cpx.
rewrite /BZprod /BZ_one /BZ_of_nat /BZopp; aw; Ytac0.
case /BZ_i0P: xz => h.
  rewrite (BZms_pr2 h); Ytac0; apply:BZm_hi_pr;qprops.
rewrite (BZp_pr2 h); Ytac0; apply:BZp_hi_pr;qprops.
Qed.

Lemma BZprod_1r x: inc x BZ -> x *z \1z = x.
Proof. by move => pa; rewrite BZprodC; apply BZprod_1l. Qed.

Hint Rewrite BZprod_1r BZprod_1l: qw.

Lemma BZprod_m1r x: inc x BZ -> x *z \1mz = BZopp x.
Proof.
move => xz; move: (CS_Bnat (BZ_pr1 xz)) => h.
rewrite /BZprod /BZ_mone /BZm_of_nat /BZ_of_nat /BZopp.
by rewrite (Y_false card1_nz); aw; Ytac0; Ytac aux.
Qed.

Lemma BZprod_m1l x: inc x BZ -> \1mz *z x = BZopp x.
Proof. by move => pa; rewrite BZprodC; apply: BZprod_m1r. Qed.

Lemma BZopp_prod_r x y: inc x BZ -> inc y BZ ->
  BZopp (x *z y) = x *z (BZopp y).
Proof.
move => pa pb.
case /BZ_i1P: (pa); first by move => ->; qw.
  move => h1; case /BZ_i1P: pb => h2;first by rewrite h2; qw.
    move:(sub_BZps_BZp h1) => h3.
    rewrite (BZprod_pp h3 (sub_BZps_BZp h2)).
    by rewrite(BZprod_pm h3 (BZopp_positive1 h2)) BZopp_pr1 BZopp_p.
  rewrite (BZprod_pm (sub_BZps_BZp h1) h2).
  rewrite (BZprod_pp (sub_BZps_BZp h1) (sub_BZps_BZp (BZopp_negative1 h2))).
  by rewrite BZopp_pr1 BZopp_m.
move => h1; case /BZ_i1P: pb => h2;first by rewrite h2; qw.
  rewrite(BZprod_mp h1 (sub_BZps_BZp h2)).
  by rewrite (BZprod_mm h1 (BZopp_positive1 h2)) BZopp_pr1 BZopp_m.
rewrite (BZprod_mm h1 h2) (BZprod_mp h1 (sub_BZps_BZp (BZopp_negative1 h2))).
by rewrite BZopp_pr1 BZopp_p.
Qed.

Lemma BZopp_prod_l x y: inc x BZ -> inc y BZ ->
    BZopp (x *z y) = (BZopp x) *z y.
Proof. by move => pa pb; rewrite BZprodC (BZopp_prod_r pb pa) BZprodC. Qed.

Lemma BZprod_opp_comm x y: inc x BZ -> inc y BZ ->
  x *z (BZopp y) = (BZopp x) *z y.
Proof. move => pa pb; rewrite - BZopp_prod_l // BZopp_prod_r //. Qed.

Lemma BZprod_opp_opp x y: inc x BZ -> inc y BZ ->
  (BZopp x) *z (BZopp y) = x *z y.
Proof. by move => pa pb; rewrite (BZprod_opp_comm (BZSo pa) pb) BZopp_K. Qed.

Lemma BZprodA x y z: inc x BZ -> inc y BZ -> inc z BZ ->
  x *z (y *z z) = (x *z y) *z z.
Proof.
move => pa pb pc; move: (BZSp pa pb) (BZSp pb pc) => pab pbc.
rewrite (BZprod_abs2 pa pbc) (BZprod_abs2 pab pc) BZprod_pr1 BZprod_pr1 cprodA.
congr (J _ _).
rewrite /BZprod_sign_aux.
case: (equal_or_not x \0z) => xz; Ytac0;first by rewrite xz; qw; Ytac0.
case: (equal_or_not z \0z) => zz; Ytac0; first by rewrite zz; qw; Ytac0; Ytac0.
case: (equal_or_not y \0z) => yz; first by rewrite yz; qw; Ytac0; Ytac0.
move: (BZprod_nz pb pc yz zz)(BZprod_nz pa pb xz yz) => yzz xyz; Ytac0; Ytac0.
rewrite (BZprod_abs2 pa pb) (BZprod_abs2 pb pc) ! pr2_pair.
rewrite /BZprod_sign_aux; Ytac0; Ytac0; Ytac0; Ytac0.
have aux: forall t, inc t BZ -> Q t = C0 \/ Q t = C1.
   by move => t /candu2P [_]; case; move => [_]; [left | right].
by case /aux: pa => ->; case /aux: pb => ->; case /aux: pc => ->;
    Ytac0; Ytac0; (try Ytac0) => //; Ytac0.
Qed.

Lemma BZprod_permute_2_in_4 a b c d:
  inc a BZ -> inc b BZ -> inc c BZ -> inc d BZ ->
  (a *z b) *z (c *z d) = (a *z c) *z (b *z d).
Proof.
move => az bz cz dz.
rewrite (BZprodA (BZSp az bz) cz dz) (BZprodC a) - (BZprodA bz az cz).
by rewrite (BZprodA (BZSp az cz) bz dz) (BZprodC b).
Qed.

Lemma BZprod_sumDr n m p: inc n BZ -> inc m BZ -> inc p BZ ->
   n *z ( m +z p) = (n *z m) +z (n *z p).
Proof.
move: n m p.
have Qa:forall n m p, inc n BZps -> inc m BZp -> inc p BZp
    -> n *z ( m +z p) = (n *z m) +z (n *z p).
  move => n m p pa pb pc.
  move: (sub_BZps_BZp pa) => pa'.
  move: (BZ_pr1(sub_BZp_BZ pa'))(BZ_pr1(sub_BZp_BZ pb))(BZ_pr1 (sub_BZp_BZ pc)).
  move => qa qb qc.
  move: (BZ_of_natp_i (BS_prod qa qb)) => qe.
  move: (BZ_of_natp_i (BS_prod qa qc)) => qf.
  rewrite (BZprod_pp pa' pb)(BZprod_pp pa' pc) (BZprod_pp pa' (BZpS_sum pb pc)).
  rewrite (BZsum_pp pb pc) (BZsum_pp qe qf). rewrite !BZ_of_nat_pr1.
  by rewrite cprod_sumDl.
have Qb:forall n m p, inc n BZps -> inc m BZp -> inc p BZ
     -> n *z ( m +z p) = (n *z m) +z (n *z p).
  move => n m p pa pb; case /BZ_i0P; last by apply: Qa.
  move => pc; move: (sub_BZps_BZp pa) => pa'.
  move: (BZ_pr1(sub_BZp_BZ pa'))(BZ_pr1(sub_BZp_BZ pb))(BZ_pr1(sub_BZms_BZ pc)).
  move => qa qb qc.
  move: (BZps_pr1nz pa) => pa''.
  have nzp:P n *c P p <> \0c by move:(BZms_hi_pr pc) => [s1 _];apply: cprod2_nz.
  move: (BZ_of_natp_i (BS_prod qa qb)) => qe.
  move: (BZm_of_natms_i (BS_prod qa qc) nzp) => qf.
  rewrite(BZsum_pm pb pc)(BZprod_pp pa' pb)(BZprod_pm pa' pc) (BZsum_pm qe qf).
  rewrite BZm_of_nat_pr1 BZ_of_nat_pr1.
  case: (card_le_to_el (CS_Bnat qc) (CS_Bnat qb)) => le1.
     have le2: (P n *c P p <=c P n *c P m) by apply: cprod_Mlele; fprops.
     Ytac0; Ytac0; rewrite (BZprod_pp pa' (BZ_of_natp_i (BS_diff _ qb))).
     by rewrite BZ_of_nat_pr1 (cdistrib_prod2_sub qa qb qc le1).
  have le1': ~(P p <=c P m) by move => h; co_tac.
  have le2': ~(P n *c P p <=c P n *c P m).
    move => bad; move: (cprod_le_simplifiable qa qc qb pa'' bad) => qg;co_tac.
  move: (BS_diff (P m) qc) => dB.
  Ytac0; Ytac0;rewrite (BZprod_pm pa' (BZm_of_natms_i dB (cdiff_nz le1))).
  by rewrite BZm_of_nat_pr1 (cdistrib_prod2_sub qa qc qb (proj1 le1)).
have Qc:forall n m p, inc n BZps -> inc m BZ -> inc p BZ
     -> n *z ( m +z p) = (n *z m) +z (n *z p).
  move => n m p pa pb pc.
  case /BZ_i0P: pb => mn; last by apply: Qb.
  move: (sub_BZms_BZ mn) (sub_BZps_BZ pa) => mz nz.
  move: (Qb _ _ _ pa (sub_BZps_BZp(BZopp_negative1 mn)) (BZSo pc)).
  move: (BZSs mz pc) (BZSp nz mz) (BZSp nz pc) => sz sa sb.
  rewrite - (BZsum_opp_distr mz pc).
  rewrite - (BZopp_prod_r nz sz) - (BZopp_prod_r nz mz) - (BZopp_prod_r nz pc).
  rewrite - (BZsum_opp_distr sa sb);apply:BZopp_inj; qprops.
have Qd: (forall x y, inc x BZ -> inc y BZ -> (BZopp y) *z x = BZopp (y *z x)).
  by move => x y xz yz; rewrite (BZopp_prod_r yz xz) (BZprod_opp_comm yz xz).
move => n m p.
case /BZ_i1P ; first by move => -> _ _; qw => //; qprops.
  by apply: Qc.
move => nz' mz pz; move: (BZopp_negative1 nz') (sub_BZms_BZ nz') => nz'' nz.
move: (sub_BZps_BZ nz'') => oz.
rewrite - (BZopp_K nz).
rewrite (Qd _ _ (BZSs mz pz) oz) (Qd _ _ mz oz) (Qd _ _ pz oz).
rewrite (Qc _ _ _ nz'' mz pz) BZsum_opp_distr; qprops.
Qed.

Lemma BZprod_sumDl n m p: inc n BZ -> inc m BZ -> inc p BZ ->
   ( m +z p) *z n = (m *z n) +z (p *z n).
Proof.
move => pa pb pc; rewrite (BZprodC) (BZprodC m) (BZprodC p).
by apply:BZprod_sumDr.
Qed.

Definition BZdiff x y := x +z (BZopp y).

Notation "x -z y" := (BZdiff x y) (at level 50).

Definition BZsucc x := x +z \1z.
Definition BZpred x := x -z \1z.

Lemma BZS_diff x y: inc x BZ -> inc y BZ -> inc (x -z y) BZ.
Proof. rewrite /BZdiff; qprops. Qed.

Hint Resolve BZS_diff: qprops.

Lemma BZS_succ x: inc x BZ -> inc (BZsucc x) BZ.
Proof. rewrite /BZsucc; qprops. Qed.

Lemma BZS_pred x: inc x BZ -> inc (BZpred x) BZ.
Proof. move => xz;rewrite /BZpred; apply:BZS_diff; qprops. Qed.

Lemma BZsucc_N x: inc x Bnat -> BZsucc (BZ_of_nat x) = BZ_of_nat (succ x).
Proof.
move => xB; rewrite /BZsucc (BZsum_pp (BZ_of_natp_i xB) (BZ_of_natp_i BS1)).
by rewrite ! BZ_of_nat_pr1 (Bsucc_rw xB).
Qed.

Lemma BZprec_N x: inc x Bnats -> BZpred (BZ_of_nat x) = BZ_of_nat (cpred x).
Proof.
move /setC1_P => [pa pb]; move: (cpred_pr pa pb) => [qa qb].
move: (BZ_of_nat_i qa) => pc.
rewrite {1} qb - (BZsucc_N qa) /BZsucc /BZpred /BZdiff.
rewrite - BZsumA; qprops. rewrite BZsum_opp_r; qw; qprops.
Qed.

Lemma BZsucc_sum a b: inc a BZ -> inc b BZ -> (BZsucc a +z b) = BZsucc (a +z b).
Proof.
move => pa pb; rewrite /BZsucc (BZsumC a) (BZsumC _ \1z) BZsumA => //; qprops.
Qed.

Lemma BZpred_sum a b: inc a BZ -> inc b BZ -> (BZpred a +z b) = BZpred (a +z b).
Proof.
move => pa pb; rewrite /BZpred/BZdiff (BZsumC a) (BZsumC _ (BZopp \1z)).
rewrite BZsumA => //; qprops.
Qed.

Section BZdiffProps.
Variables (x y z: Set).
Hypotheses (xz: inc x BZ)(yz: inc y BZ)(zz: inc z BZ).

Lemma BZsucc_pred : BZsucc (BZpred x) = x.
Proof.
rewrite /BZsucc /BZpred /BZdiff.
rewrite - BZsumA; qprops; rewrite BZsum_opp_l; qw; qprops.
Qed.

Lemma BZpred_succ: BZpred (BZsucc x) = x.
Proof.
rewrite /BZsucc /BZpred /BZdiff; rewrite - BZsumA; qprops.
rewrite BZsum_opp_r; qw; qprops.
Qed.

Lemma BZdiff_sum: (x +z y) -z x = y.
Proof. by rewrite /BZdiff BZsumC (BZsumA (BZSo xz) xz yz); qw. Qed.

Lemma BZsum_diff: x +z (y -z x) = y.
Proof. by rewrite /BZdiff (BZsumC y) (BZsumA xz (BZSo xz) yz); qw. Qed.

Lemma BZdiff_diag : x -z x = \0z.
Proof. by rewrite /BZdiff; qw. Qed.

Lemma BZdiff_0r: x -z \0z = x.
Proof. by rewrite / BZdiff; qw. Qed.

Lemma BZdiff_0l: \0z -z x = BZopp x.
Proof. rewrite /BZdiff; qw; qprops. Qed.

Lemma BZdiff_sum_simpl_l: (x +z y) -z (x +z z) = y -z z.
Proof.
rewrite /BZdiff (BZsum_opp_distr xz zz) (BZsumC x y).
rewrite (BZsumA (BZSs yz xz) (BZSo xz) (BZSo zz)).
by rewrite -(BZsumA yz xz (BZSo xz)); qw.
Qed.

Lemma BZdiff_sum_comm: (x +z y) -z z = (x -z z) +z y.
Proof. rewrite /BZdiff (BZsumC x y) (BZsumC _ y) - (BZsumA yz xz); qprops. Qed.

Lemma BZopp_diff: BZopp (x -z y) = y -z x.
Proof.
rewrite /BZdiff (BZsum_opp_distr xz (BZSo yz)).
by rewrite (BZopp_K yz) BZsumC.
Qed.

End BZdiffProps.

Section BZdiffProps2.
Variables (x y z: Set).
Hypotheses (xz: inc x BZ)(yz: inc y BZ)(zz: inc z BZ).

Lemma BZsucc_disc: x <> BZsucc x.
Proof.
move: BZS1 => pb pc.
move:(BZdiff_sum xz pb); rewrite - /(BZsucc x) - pc (BZdiff_diag xz) => h.
by case: BZ_one_not_zero; rewrite h.
Qed.

Lemma BZsum_diff_ea: x = y +z z -> z = x -z y.
Proof. by move => -> ; rewrite BZdiff_sum. Qed.

Lemma BZdiff_diag_rw: x -z y = \0z -> x = y.
Proof.
by move => h; move:(f_equal (BZsum y) h); rewrite (BZsum_diff yz xz); qw.
Qed.

Lemma BZdiff_sum_simpl_r: (x +z z) -z (y +z z) = x -z y.
Proof. by rewrite (BZsumC x z) (BZsumC y z); apply: BZdiff_sum_simpl_l. Qed.

Lemma BZdiff_succ_l: BZsucc (x -z y) = (BZsucc x) -z y.
Proof. rewrite /BZsucc; symmetry; apply: BZdiff_sum_comm;qprops. Qed.

Lemma BZsum_reg_r: x +z z = y +z z -> x = y.
Proof.
move => h; rewrite - (BZdiff_sum zz xz) - (BZdiff_sum zz yz).
by rewrite BZsumC h BZsumC.
Qed.

Lemma BZsum_reg_l: x +z y = x +z z -> y = z.
Proof.
by move => h; rewrite - (BZdiff_sum xz yz) - (BZdiff_sum xz zz) h.
Qed.

End BZdiffProps2.

Lemma BZprod_diff_Dr x y z: inc x BZ -> inc y BZ -> inc z BZ ->
   x *z (y -z z) = (x *z y) -z (x *z z).
Proof.
move => xz yz zz; rewrite /BZdiff (BZprod_sumDr xz yz (BZSo zz)).
by rewrite BZopp_prod_r.
Qed.

Lemma BZprod_diff_Dl x y z: inc x BZ -> inc y BZ -> inc z BZ ->
  (y -z z) *z x = (y *z x) -z (z *z x).
Proof.
by move => xz yz zz; rewrite BZprodC (BZprodC y) (BZprodC z) BZprod_diff_Dr.
Qed.

Lemma BZprod_reg_r x y z: inc x BZ -> inc y BZ -> inc z BZ -> z <> \0z ->
   x *z z = y *z z -> x = y.
Proof.
move => xz yz zz znz eq; apply: (BZdiff_diag_rw xz yz); ex_middle bad.
case: (BZprod_nz (BZS_diff xz yz) zz bad znz).
by move:(BZprod_diff_Dl zz xz yz); rewrite eq (BZdiff_diag (BZSp yz zz)).
Qed.

Lemma BZprod_reg_l x y z: inc x BZ -> inc y BZ -> inc z BZ -> z <> \0z ->
   z *z x = z *z y -> x = y.
Proof.
by move => xz yz zz znz; rewrite BZprodC (BZprodC z); apply: BZprod_reg_r.
Qed.

Lemma BZprod_1_inversion_l x y : inc x BZ -> inc y BZ -> x *z y = \1z ->
   (x = y /\ (x = \1z \/ x = \1mz)).
Proof.
move => xz yz; rewrite (BZprod_abs2 xz yz) => h; move: (pr1_def h) => h1.
move :(BZ_pr1 xz) (BZ_pr1 yz) => pa pb.
case: (equal_or_not (P x) \0c) => xnz.
  by move: h1; rewrite xnz cprodC cprod0r=> bad; case: card1_nz.
case: (equal_or_not (P y) \0c) => ynz.
  by move: h1; rewrite ynz cprod0r=> bad; case: card1_nz.
case: (equal_or_not (P x) \1c) => px1; last first.
   move: (card_ge2 (CS_Bnat pa) xnz px1) => le1.
   move: (card_ge1 (CS_Bnat pb) ynz) card_lt_12 => le2 le3.
   move: (cprod_Mlele le1 le2); rewrite h1; aw; [move => l4;co_tac | fprops].
have py1: P y = P x by move: h1; rewrite px1 (cprod1l(CS_Bnat pb)).
move: (pr2_def h); rewrite /BZprod_sign_aux.
Ytac pc; first by case: xnz; rewrite pc /BZ_zero /BZ_of_nat;aw.
Ytac pd; first by case: ynz; rewrite pd /BZ_zero /BZ_of_nat;aw.
Ytac pe; last by move => bad;case: TP_ne.
move => _; move /candu2P: xz => [prx etx]; move /candu2P: yz => [pry _]; split.
  by apply: pair_exten.
case: etx; move=> [_ qx].
right; move: card1_nz => h3;rewrite /BZ_mone /BZm_of_nat; Ytac0.
  apply: pair_exten; aw; fprops.
left; rewrite /BZ_one /BZ_of_nat; apply: pair_exten; aw; fprops.
Qed.

Lemma BZprod_1_inversion_more a b c:
  inc a BZ -> inc b BZ -> inc c BZ -> a = a *z (b *z c) ->
  [\/ a = \0z, b = \1z | b = \1mz].
Proof.
move => az bz cz.
rewrite - {1} (BZprod_1r az) => h.
case: (equal_or_not a \0z) => anz;first by constructor 1.
move: (BZprod_reg_l BZS1 (BZSp bz cz) az anz h) => h1; symmetry in h1.
move: (BZprod_1_inversion_l bz cz h1) => [_]; case =>H; in_TP4.
Qed.

Lemma BZsum_xx n : inc n BZ -> n +z n = n *z \2z.
Proof.
move => nz; rewrite BZprodC.
have aux: inc \2z BZp by apply: BZ_of_natp_i; fprops.
have Ha: forall m, inc m BZp -> m +z m = \2z *z m.
   move => m mp; rewrite (BZsum_pp mp mp) - two_times_n (BZprod_pp aux mp).
   rewrite /BZ_two /BZ_of_nat; aw.
case /BZ_i0P: nz => sx; last by apply: Ha.
move: (sub_BZps_BZp (BZopp_negative1 sx)) => pa.
move: (sub_BZp_BZ pa) => pb.
rewrite - (BZopp_K (sub_BZms_BZ sx)) - (BZsum_opp_distr pb pb) (Ha _ pa).
by move: (BZopp_prod_r BZS2 pb).
Qed.

Lemma BZprod_succ_r n m: inc n BZ -> inc m BZ ->
   n *z (BZsucc m) = (n *z m) +z n.
Proof.
by move => pa pb; rewrite /BZsucc (BZprod_sumDr pa pb BZS1) BZprod_1r.
Qed.

Lemma BZprodt_succ_l n m: inc n BZ -> inc m BZ ->
  (BZsucc n) *z m = (n *z m) +z m.
Proof. by move => pa pb; rewrite BZprodC (BZprod_succ_r pb pa) BZprodC. Qed.

The sign function


Definition BZsign x:= Yo (P x = \0c) \0z (Yo (Q x = C1) \1z \1mz).

Lemma BZsign_trichotomy a: BZsign a = \1z \/ BZsign a = \1mz \/ BZsign a = \0z.
Proof. rewrite /BZsign; Ytac pa; try Ytac pb; fprops. Qed.

Lemma BZS_sign x: inc (BZsign x) BZ.
Proof. rewrite /BZsign; Ytac pa;[ qprops | Ytac pb; qprops ]. Qed.

Hint Resolve BZS_sign: qprops.

Lemma BZsign_pos x: inc x BZps -> BZsign x = \1z.
Proof.
by rewrite /BZsign; move /indexed_P=> [_ ] /setC1_P [_ nz] q; Ytac0; Ytac0.
Qed.

Lemma BZsign_neg x: inc x BZms -> BZsign x = BZ_mone.
Proof.
by rewrite /BZsign; move /indexed_P=> [_] /setC1_P [_ nz] ->; Ytac0; Ytac0.
Qed.

Lemma BZsign_0: BZsign \0z = \0z.
Proof. by rewrite /BZsign BZ0_pr1; Ytac0. Qed.

Lemma BZabs_sign x: inc x BZ -> x = (BZsign x) *z (BZabs x).
Proof.
move => xz; move: (BZSa xz) => az.
case /BZ_i1P: (xz) => xs; first by rewrite xs; qw.
  by rewrite (BZsign_pos xs) (BZabs_pos (sub_BZps_BZp xs)); qw.
by rewrite (BZsign_neg xs) (BZabs_neg xs) (BZprod_m1l (BZSo xz)) (BZopp_K xz).
Qed.

Lemma BZsign_abs x: inc x BZ -> x *z (BZsign x) = BZabs x.
Proof.
move => xz; move: (BZS_sign x) => xsp.
case /BZ_i1P: (xz) => xs; first by rewrite xs; qw.
  by rewrite (BZsign_pos xs) (BZabs_pos (sub_BZps_BZp xs)); qw.
by rewrite (BZsign_neg xs) (BZabs_neg xs) (BZprod_m1r xz).
Qed.

Lemma BZprod_sign x y: inc x BZ -> inc y BZ ->
  BZsign (x *z y) = (BZsign x) *z (BZsign y).
Proof.
move => xz yz.
case:(equal_or_not x \0z) => xnz; first by rewrite xnz; qw;rewrite BZsign_0; qw.
case:(equal_or_not y \0z) => ynz; first by rewrite ynz; qw;rewrite BZsign_0; qw.
rewrite (BZprod_abs2 xz yz) /BZprod_sign_aux /BZsign pr1_pair pr2_pair.
have pxnz: (P x) <> \0c by move => h; case: xnz; exact (BZ_0_if_abs0 xz h).
have pynz: (P y) <> \0c by move => h; case: ynz; exact (BZ_0_if_abs0 yz h).
move: (cprod2_nz pxnz pynz) => pxynz.
Ytac0; Ytac0; Ytac0; Ytac0; Ytac0.
move: BZS1 BZSm1 => ha hb.
case: (equal_or_not (Q x) (Q y)) => sq; Ytac0; Ytac0.
  by rewrite - sq; Ytac qa; [ qw | rewrite (BZprod_m1r hb) BZopp_m1 ].
move: sq;case /BZ_pr2: xz => ->; Ytac0.
case /BZ_pr2: yz => ->; Ytac0; qw => //.
case /BZ_pr2: yz => ->; Ytac0; qw => //.
Qed.

Lemma BZ_le_diffP a b: inc a BZ -> inc b BZ -> (a <=z b <-> inc (b -z a) BZp).
Proof.
pose aux a b := (a <=z b <-> inc (b -z a) BZp).
move: a b.
have Ha: (forall a b, inc a BZp -> inc b BZp -> aux a b).
  move => a b az bz.
  move: (sub_BZp_BZ bz) => bz1.
  move: (BZ_pr1 (sub_BZp_BZ az)) (BZ_pr1 bz1) => pa pb.
  rewrite /aux; apply: (iff_trans (BZ_le_P1 az bz)).
  case: (equal_or_not a \0z) => anz.
    rewrite anz /BZdiff BZopp_0; qw => //; split => h //; fprops.
  have az1: inc a BZps by apply /BZps_iP.
  move:(BZopp_positive1 az1) => az2;rewrite /BZdiff.
  move: (BZopp_pr1 a)=> eq0.
  case: (card_le_to_el (CS_Bnat pa) (CS_Bnat pb)) => ce1.
     split; [move => _ | by done].
     move: (BZsum_pm1 bz az2); rewrite eq0 => h; rewrite (h ce1).
     apply: BZ_of_natp_i; fprops.
  split; first by move => h; co_tac.
  move: (cdiff_nz ce1) => ne1.
  rewrite -eq0 in ce1; rewrite (BZsum_pm2 bz az2 ce1); rewrite eq0.
  by rewrite /BZm_of_nat;Ytac0 => bad; move:(BZp_pr2 bad); aw => ba; case:TP_ne.
have Hb: (forall a b, inc a BZ -> inc b BZp -> aux a b).
  move => a b pa pb; case /BZ_i0P: pa => ap; last by apply: Ha.
  split => _; first by apply: (BZpS_sum pb (sub_BZps_BZp (BZopp_negative1 ap))).
  exact (proj1 (BZ_le_pr2 pb ap)).
move => a b az bz.
case /BZ_i0P: (bz) => bz1; last by apply: Hb.
case /BZ_i0P: (az) => az1; last first.
  split; move => ha; first by case: (BZ_le_pr4 az1 bz1).
  by move:(BZ_di_neg_pos (BZmsS_sum_l bz1 (BZopp_positive2 az1)) ha).
move: (sub_BZps_BZp (BZopp_negative1 az1)) => tt.
move: (Hb _ _ (BZSo bz) tt) => aux1.
have ->: b -z a = (BZopp a -z BZopp b) by rewrite /BZdiff BZsumC (BZopp_K bz).
split => ha.
  by move: (BZ_le_opp ha); move /aux1.
by move/aux1: ha => hb; move: (BZ_le_opp hb); rewrite (BZopp_K az)(BZopp_K bz).
Qed.

Lemma BZ_le_diffP1 a b: inc a BZ -> inc b BZ ->
  (a <=z b <-> \0z <=z (b -z a)).
Proof.
move => pa pb; apply: (iff_trans (BZ_le_diffP pa pb)).
symmetry; apply: BZ_positive_P.
Qed.

Lemma BZ_lt_diffP a b: inc a BZ -> inc b BZ ->
  (a <z b <-> inc (b -z a) BZps).
Proof.
move => pa pb; split.
  move => [] /(BZ_le_diffP pa pb) => pc pd; apply /BZps_iP;split => //.
  dneg aux; symmetry; exact (BZdiff_diag_rw pb pa aux).
move /BZps_iP => [] /(BZ_le_diffP pa pb) pc pd; split => //.
by dneg aux; rewrite aux (BZdiff_diag pb).
Qed.

Lemma BZ_lt_diffP1 a b: inc a BZ -> inc b BZ ->
  (a <z b <-> \0z <z (b -z a)).
Proof.
move => pa pb; apply: (iff_trans (BZ_lt_diffP pa pb)).
symmetry; apply: BZ_positive_P1.
Qed.

Lemma BZ_lt_diffP2 a b: inc a BZ -> inc b BZ ->
  (a <z b <-> inc (a -z b) BZms).
Proof.
move => pa pb; apply: (iff_trans (BZ_lt_diffP pa pb)).
rewrite - (BZopp_diff pb pa); split => h.
  apply: BZopp_positive1; qprops.
rewrite - (BZopp_K (BZS_diff pb pa)); apply: (BZopp_negative1 h).
Qed.

Lemma BZsum_Meqle a b c: inc a BZ -> inc b BZ -> inc c BZ ->
  (a <=z b <-> (c +z a) <=z (c +z b)).
Proof.
move => pa pb pc.
apply: (iff_trans (BZ_le_diffP pa pb)); apply: iff_sym.
apply: (iff_trans (BZ_le_diffP (BZSs pc pa) (BZSs pc pb))).
by rewrite BZdiff_sum_simpl_l.
Qed.

Lemma BZsum_Mleeq a b c: inc a BZ -> inc b BZ -> inc c BZ
  -> (a <=z b <-> (a +z c) <=z (b +z c)).
Proof.
by move => pa pb pc; rewrite (BZsumC a c) (BZsumC b c); apply: BZsum_Meqle.
Qed.

Lemma BZsum_Meqlt a b c: inc a BZ -> inc b BZ -> inc c BZ ->
  (a <z b <-> (c +z a) <z (c +z b)).
move => pa pb pc.
apply: (iff_trans (BZ_lt_diffP pa pb)); apply: iff_sym.
apply: (iff_trans (BZ_lt_diffP (BZSs pc pa) (BZSs pc pb))).
by rewrite BZdiff_sum_simpl_l.
Qed.

Lemma BZsum_Mlteq a b c: inc a BZ -> inc b BZ -> inc c BZ
  -> (a <z b <-> (a +z c) <z (b +z c)).
Proof.
by move => pa pb pc; rewrite (BZsumC a c) (BZsumC b c); apply: BZsum_Meqlt.
Qed.

Lemma BZ_induction_pos a (r:property):
  (r a) -> (forall n, a <=z n -> r n -> r (BZsucc n))
  -> (forall n, a <=z n -> r n).
Proof.
move => pb pc n h; move: (h) => [pa pd _].
move /(BZ_le_diffP pa pd):h => dp.
rewrite - (BZsum_diff pa pd) BZsumC - (BZp_hi_pr dp).
move : (BZ_pr1 (sub_BZp_BZ dp)) => xn.
pose s n := r ((BZ_of_nat n) +z a); rewrite -/(s _).
apply: (cardinal_c_induction _ _ xn).
  by rewrite /s -/BZ_zero; qw.
move => m mb; move:(BZ_of_natp_i mb) => aux1; move: (sub_BZp_BZ aux1) => aux.
have : a <=z (BZ_of_nat m +z a).
  by apply/(BZ_le_diffP pa (BZSs aux pa)); rewrite BZsumC (BZdiff_sum pa aux).
rewrite /s - (BZsucc_N mb) (BZsucc_sum (BZ_of_nat_i mb) pa);apply:pc.
Qed.

Lemma BZ_induction_neg a (r:property):
  (r a) -> (forall n, n <=z a -> r n -> r (BZpred n))
  -> (forall n, n <=z a -> r n).
Proof.
move => pb pc n h; move: (h) => [pa pd _].
move: (BZ_le_opp h) => pe.
rewrite - (BZopp_K pa); pose s n:= r (BZopp n); rewrite -/(s _).
move: pb ; rewrite - (BZopp_K pd); rewrite -/(s _) => sa.
apply: (BZ_induction_pos sa _ pe).
move => m le1. move: (BZ_le_opp le1); rewrite (BZopp_K pd) /s /BZsucc.
rewrite (BZsum_opp_distr (proj32 le1) BZS1); apply: pc.
Qed.

Lemma BZ_ind1 a (p:property):
  inc a BZ -> p a ->
  (forall x, BZ_le a x -> p x -> p (BZsucc x)) ->
  (forall x, BZ_le x a -> p x -> p (BZpred x)) ->
  forall n, inc n BZ -> p n.
Proof.
move => az pa pb pc n nz; case: (BZ_le_to_ee az nz).
  by apply:BZ_induction_pos.
by apply:BZ_induction_neg.
Qed.

Lemma BZ_ind (p:property):
  p \0z ->
  (forall x, inc x BZ -> p x -> p (BZsucc x)) ->
  (forall x, inc x BZ -> p x -> p (BZpred x)) ->
  forall n, inc n BZ -> p n.
Proof.
move: BZS0 => pa pb pc pd n nz; apply: (BZ_ind1 pa pb _ _ nz).
  by move=> x [_ xb _]; apply: pc.
by move=> x [xb _ _]; apply: pd.
Qed.

Definition BZ_of_Z (n:int) :=
  match n with
    | Posz p => BZ_of_nat (nat_to_B p)
    | Negz p => BZm_of_nat (nat_to_B p.+1)
end.

Section Conversions.

Require Import ssralg ssrnum.
Import GRing.Theory.
Local Open Scope ring_scope.

Lemma BZ_of_Z_inc x: inc (BZ_of_Z x) BZ.
Proof.
case: x; move => p /=.
  apply:BZ_of_nat_i;apply: nat_to_B_Bnat.
  apply:BZm_of_nat_i; apply: BS_succ;apply: nat_to_B_Bnat.
Qed.

Lemma positive_non_zero1 p :
  inc (BZ_of_nat (nat_to_B p)) BZp.
Proof. by apply:BZ_of_natp_i; apply:nat_to_B_Bnat. Qed.

Lemma positive_non_zero2 p :
  inc (BZm_of_nat (succ (nat_to_B p))) BZms.
Proof.
apply: BZm_of_natms_i; first by apply: BS_succ;apply: nat_to_B_Bnat.
apply: succ_nz.
Qed.

Lemma positive_non_zero2bis p :
  inc (BZm_of_nat (nat_to_B p.+1)) BZms.
Proof. exact: (positive_non_zero2 p). Qed.

Lemma BZ_of_Z_injective x y : BZ_of_Z x = BZ_of_Z y -> x = y.
Proof.
case: x; case: y; simpl => n m /= eq.
- by move:(nat_to_B_injective (BZ_of_nat_inj eq)) => ->.
- move: (positive_non_zero1 m) (positive_non_zero2 n); rewrite -eq => pa pb.
  case: (BZ_di_neg_pos pb pa).
- move: (positive_non_zero1 n) (positive_non_zero2 m); rewrite -eq => pa pb.
  case: (BZ_di_neg_pos pb pa).
- have pa: cardinalp (nat_to_B m) by move: (nat_to_B_Bnat m) => h; fprops.
  have pb: cardinalp (nat_to_B n) by move: (nat_to_B_Bnat n) => h; fprops.
  move:(succ_injective1 pa pb (BZm_of_nat_inj eq)) => eq2.
  by rewrite (nat_to_B_injective eq2).
Qed.

Lemma BZ_of_Z_surjective x : inc x BZ -> exists y, BZ_of_Z y = x.
Proof.
case /BZ_i0P => pa.
  move: (BZms_hi_pr pa) => [_ <- ].
  move /indexed_P: pa => [_ pc _]; move/setC1_P: pc => [pB pnz].
  move: (cpred_pr pB pnz) => []; set c := cpred _ => ca ->.
  by move: (nat_to_B_surjective ca) => [n ->];exists (Negz n).
rewrite - (BZp_hi_pr pa).
move /indexed_P: pa => [_ pc _].
move: (nat_to_B_surjective pc) => [n ->]; by exists n.
Qed.

Definition BZ_of_Z_aux p := Bo (BZ_of_Z_inc p).

Lemma BZ_of_Z_aux_bijection: bijectiveC BZ_of_Z_aux.
Proof.
split.
  move => a b sv; move: (f_equal (@Ro BZ) sv); rewrite ! B_eq => sv1.
  by apply:BZ_of_Z_injective.
move => t; move: (R_inc t) => t1; move: (BZ_of_Z_surjective t1).
by move => [v h]; exists v; apply: R_inj; rewrite B_eq.
Qed.

Definition Z_of_BZ x (H: inc x BZ) := inverseC (BZ_of_Z_aux_bijection) (Bo H).

Lemma Z_of_BZ_pa x (H: inc x BZ): (BZ_of_Z (Z_of_BZ H)) = x.
Proof.
rewrite /Z_of_BZ.
move: (inverseC_prb (BZ_of_Z_aux_bijection) (Bo H)) => pa.
by move: (f_equal (@Ro BZ) pa); rewrite ! B_eq.
Qed.

Lemma Z_of_BZ_pb p : Z_of_BZ (BZ_of_Z_inc p) = p.
Proof. by move:(inverseC_pra BZ_of_Z_aux_bijection p). Qed.

Lemma BZ_Z_0: BZ_of_Z 0 = \0z. Proof. trivial. Qed.
Lemma BZ_Z_1: BZ_of_Z 1%Z = \1z.
Proof. by simpl; rewrite succ_zero. Qed.

Lemma BZ_Z_m1: BZ_of_Z (- 1%:Z) = \1mz.
Proof. by simpl; rewrite succ_zero. Qed.

Lemma Z_of_BZ_zero: Z_of_BZ BZS0 = 0%Z.
Proof. by apply:BZ_of_Z_injective; rewrite BZ_Z_0 Z_of_BZ_pa. Qed.

Lemma Z_of_BZ_one: Z_of_BZ BZS1 = 1%Z.
Proof. by apply:BZ_of_Z_injective; rewrite BZ_Z_1 Z_of_BZ_pa. Qed.

Lemma Z_of_BZ_mone: Z_of_BZ BZSm1 = (-1)%Z.
Proof. by apply:BZ_of_Z_injective; rewrite BZ_Z_m1 Z_of_BZ_pa. Qed.

Lemma BZ_of_Z_opp x: BZ_of_Z (- x) = BZopp (BZ_of_Z x).
Proof.
case: x => p; simpl; last by rewrite BZopp_m //.
by rewrite BZopp_p; case: p => //=; rewrite /BZm_of_nat; Ytac0.
Qed.

Lemma BZ_of_Z_neg p: BZ_of_Z (Negz p) = BZopp (BZ_of_Z (Posz p.+1)).
Proof.
simpl. set t := (succ (nat_to_B p)).
by rewrite /BZopp /BZ_of_nat; aw; Ytac0.
Qed.

Lemma BZ_of_Z_abs x: BZ_of_Z (`|x|) = BZabs (BZ_of_Z x).
Proof.
case: x; simpl => p.
  by rewrite BZabs_pos //; apply:(positive_non_zero1 p).
move: (@succ_nz (nat_to_B p)) => snz.
rewrite /BZm_of_nat /BZabs; Ytac0;aw.
Qed.

Lemma BZ_of_Z_sign (x:int): BZ_of_Z (Num.sg x) = BZsign (BZ_of_Z x).
Proof.
case: x => /= p.
  rewrite sgrEz;case: p => /=; first by rewrite BZsign_0.
  move => p; rewrite (BZsign_pos) ? succ_zero //.
  apply/BZps_iP; split.
    apply: BZ_of_natp_i; apply: BS_succ; apply: nat_to_B_Bnat.
  move=> h; move: (f_equal P h); rewrite BZ_of_nat_pr1 BZ0_pr1;apply: succ_nz.
rewrite (BZsign_neg (positive_non_zero2 p)) succ_zero //.
Qed.

Lemma BZ_of_Z_prod x y: BZ_of_Z (x * y) = (BZ_of_Z x) *z (BZ_of_Z y).
Proof.
have ppc:forall n m: nat, BZ_of_Z (Posz n * Posz m) = BZ_of_Z n *z BZ_of_Z m.
 move => n m; move: (positive_non_zero1 n)(positive_non_zero1 m) => pa pb.
 by simpl;rewrite (BZprod_pp pa pb) !BZ_of_nat_pr1 nat_to_B_prod.
have npc: forall n (m:nat), BZ_of_Z (Posz m * Negz n) =
    BZ_of_Z m *z BZ_of_Z (Negz n).
  move => n m; rewrite BZ_of_Z_neg - BZopp_prod_r;try apply:BZ_of_Z_inc.
  by rewrite - ppc NegzE mulrN BZ_of_Z_opp.
move; case: x; case: y => n m.
- by apply: ppc.
- apply: npc.
- rewrite BZprodC mulrC; apply: npc.
- move: (positive_non_zero2bis n)(positive_non_zero2bis m) => pa pb.
  rewrite (BZprod_mm pb pa) ! BZm_of_nat_pr1 - nat_to_B_prod //.
Qed.

Lemma BZ_of_Z_succ (x:int): BZ_of_Z (1 + x) = \1z +z BZ_of_Z x.
Proof.
have cp:forall (n: nat), BZ_of_Z (1 + (Posz n)) = \1z +z BZ_of_Z n.
  move => n.
  have pa: cardinalp (nat_to_B n) by move: (nat_to_B_Bnat n) => h; fprops.
  simpl; rewrite (BZsum_pp (sub_BZps_BZp BZps1) (positive_non_zero1 n)).
  rewrite 2!BZ_of_nat_pr1 csumC card_succ_pr4 //.
case: x=> // n.
rewrite BZ_of_Z_neg NegzE.
have ->: Posz(n.+1) = 1 + Posz n by [].
have nz := (BZ_of_Z_inc n).
rewrite cp (BZsum_opp_distr BZS1 nz) (BZsumA BZS1 (BZSo BZS1) (BZSo nz)).
rewrite (BZsum_opp_r BZS1) (BZsum_0l (BZSo nz)) - BZ_of_Z_opp opprD.
by rewrite - {1} (opprK 1) addKr.
Qed.

Lemma BZ_of_Z_sum (x y: int): BZ_of_Z (x + y) = (BZ_of_Z x) +z (BZ_of_Z y).
Proof.
move: x y; apply: int_rec.
   move => y; rewrite add0r /= BZsum_0l //; apply:BZ_of_Z_inc.
move => n Hrec y.
  have ->: BZ_of_Z n.+1 = (BZ_of_Z n) +z \1z by rewrite BZsumC - BZ_of_Z_succ.
  have ->: (Posz(n.+1) + y) = 1 + (Posz n + y) by rewrite addrA; congr (_ + _).
  rewrite BZ_of_Z_succ (BZsumC _ \1z).
  rewrite - BZsumA ? Hrec //; qprops; apply: BZ_of_Z_inc.
move => n Hrec y.
have nz := (BZ_of_Z_inc n).
have ynz := (BZ_of_Z_inc (y-1)).
rewrite addrC - opprB (BZ_of_Z_opp n.+1).
have ->: (Posz(n.+1) - y) = 1 + (Posz n - y) by rewrite addrA; congr (_ + _).
have ->: Posz(n.+1) = 1 + Posz n by [].
have aux : y = 1 + (y - 1) by rewrite addrC (subrK 1 y).
rewrite opprD opprB addrC (addrC y) - addrA Hrec.
rewrite {2} aux BZ_of_Z_opp 2! BZ_of_Z_succ (BZsum_opp_distr BZS1 nz).
rewrite (BZsum_permute_2_in_4 (BZSo BZS1) (BZSo nz) BZS1 ynz).
rewrite (BZsum_opp_l BZS1) BZsum_0l //; apply: (BZSs (BZSo nz) ynz).
Qed.

Lemma BZ_of_Z_diff x y: BZ_of_Z (x - y) = (BZ_of_Z x) -z (BZ_of_Z y).
Proof. rewrite BZ_of_Z_sum BZ_of_Z_opp //. Qed.

Lemma BZ_of_Z_pred (x:int): BZ_of_Z (x -1) = BZ_of_Z x -z \1z.
Proof. by rewrite BZ_of_Z_diff BZ_Z_1. Qed.

Lemma BZ_of_Z_le (x y: int): x <= y <-> ( (BZ_of_Z x) <=z (BZ_of_Z y)).
Proof.
have aux: forall (z:int), inc (BZ_of_Z z) BZp <-> 0 <= z.
  case => n.
    rewrite le0z_nat; split => // _; exact (positive_non_zero1 n).
  split => h.
    by move: (BZ_di_neg_pos (positive_non_zero2 n) h).
  discriminate h.
apply: iff_sym.
apply: (iff_trans (BZ_le_diffP (BZ_of_Z_inc x) (BZ_of_Z_inc y))).
by rewrite - BZ_of_Z_diff - Num.Theory.subr_ge0.
Qed.

Lemma BZ_of_Z_lt (x y:int): x < y <-> ( (BZ_of_Z x) <z (BZ_of_Z y)).
Proof.
rewrite Num.Theory.ltr_neqAle; split=> //.
  move/andP => [p1 /BZ_of_Z_le p2]; split => // eq.
  by move /eqP: p1; case; apply:BZ_of_Z_injective.
case; move /BZ_of_Z_le => p1 p2; apply /andP; split => //.
by apply /eqP => eq; case: p2; rewrite eq.
Qed.

End Conversions.

More comparision

Lemma BZsum_Mlele a b c d: a <=z c -> b <=z d -> (a +z b) <=z (c +z d).
Proof.
move => eq1 eq2; move: (proj32 eq1) (proj31 eq2)=> cz bz.
move /(BZsum_Mleeq (proj31 eq1) cz bz): eq1 => eq3.
move/(BZsum_Meqle bz (proj32 eq2) cz): eq2 => eq4.
BZo_tac.
Qed.

Lemma BZsum_Mlelt a b c d: a <=z c -> b <z d -> (a +z b) <z (c +z d).
Proof.
move => eq1 eq2; move: (proj32 eq1) (proj31_1 eq2)=> cz bz.
move /(BZsum_Mleeq (proj31 eq1) cz bz): eq1 => eq3.
move/(BZsum_Meqlt bz (proj32_1 eq2) cz): eq2 => eq4.
BZo_tac.
Qed.

Lemma BZsum_Mltle a b c d: a <z c -> b <=z d -> (a +z b) <z (c +z d).
Proof.
by move => eq1 eq2; rewrite (BZsumC a)(BZsumC c); apply:BZsum_Mlelt.
Qed.

Lemma BZsum_Mltlt a b c d: a <z c -> b <z d -> (a +z b) <z (c +z d).
Proof. by move => eq1 [eq2 _]; apply: BZsum_Mltle. Qed.

Lemma BZsum_Mlege0 a c d: a <=z c -> \0z <=z d -> a <=z (c +z d).
Proof.
move => pa pb; move: (BZsum_Mlele pa pb); qw => //; exact (proj31 pa).
Qed.

Lemma BZsum_Mlegt0 a c d: a <=z c -> \0z <z d -> a <z (c +z d).
Proof.
move => pa pb; move: (BZsum_Mlelt pa pb); qw => //; exact (proj31 pa).
Qed.

Lemma BZsum_Mltge0 a c d: a <z c -> \0z <=z d -> a <z (c +z d).
Proof.
move => pa pb; move: (BZsum_Mltle pa pb); qw => //; exact (proj31_1 pa).
Qed.

Lemma BZsum_Mltgt0 a c d: a <z c -> \0z <z d -> a <z (c +z d).
Proof.
move => pa pb; move: (BZsum_Mltlt pa pb); qw => //; exact (proj31_1 pa).
Qed.

Lemma BZsum_Mlele0 a b c : a <=z c -> b <=z \0z -> (a +z b) <=z c.
Proof.
move => pa pb; move: (BZsum_Mlele pa pb); qw => //; exact (proj32 pa).
Qed.

Lemma BZsum_Mlelt0 a b c : a <=z c -> b <z \0z -> (a +z b) <z c.
Proof.
move => pa pb; move: (BZsum_Mlelt pa pb); qw => //; exact (proj32 pa).
Qed.

Lemma BZsum_Mltle0 a b c : a <z c -> b <=z \0z -> (a +z b) <z c.
Proof.
move => pa pb; move: (BZsum_Mltle pa pb); qw => //; exact (proj32_1 pa).
Qed.

Lemma BZsum_Mltlt0 a b c : a <z c -> b <z \0z -> (a +z b) <z c.
Proof.
move => pa pb; move: (BZsum_Mltlt pa pb); qw => //; exact (proj32_1 pa).
Qed.

Lemma BZ_sum_Mp a b: inc a BZ -> inc b BZp -> a <=z (a +z b).
Proof.
move => pa pb.
move /BZ_positive_P: pb => eq1; exact:(BZsum_Mlege0 (BZ_leR pa) eq1).
Qed.

Lemma BZ_sum_Mps a b: inc a BZ -> inc b BZps -> a <z (a +z b).
Proof.
move => pa pb.
move /BZ_positive_P1: pb => eq1; exact:(BZsum_Mlegt0 (BZ_leR pa) eq1).
Qed.

Lemma BZ_sum_Mm a b: inc a BZ -> inc b BZm-> (a +z b) <=z a.
Proof.
move => pa pb.
by move /BZ_negative_P1: pb => eq1; move:(BZsum_Mlele0 (BZ_leR pa) eq1).
Qed.

Lemma BZ_sum_Mms a b: inc a BZ -> inc b BZms -> (a +z b) <z a.
Proof.
move => pa pb.
by move /BZ_negative_P: pb => eq1; move:(BZsum_Mlelt0 (BZ_leR pa) eq1).
Qed.

Lemma BZ_lt_succ n: inc n BZ -> n <z (BZsucc n).
Proof.
move => nz; rewrite /BZsucc; apply: BZ_sum_Mps => //; apply: BZps1.
Qed.

Lemma BZ_lt_pred n: inc n BZ -> (BZpred n) <z n.
Proof.
by move => nz; rewrite -{2} (BZsucc_pred nz);apply: BZ_lt_succ;apply: BZS_pred.
Qed.

Lemma BZ_lt_succ1P a b: inc a BZ -> inc b BZ ->
  (a <z (BZsucc b) <-> a <=z b).
Proof.
move => pa pb; split; last first.
  have h: inc (\1z -z \0z) BZps by rewrite /BZdiff; qw; qprops;apply: BZps1.
  have: \0z <z \1z by apply/ (BZ_lt_diffP BZS0 BZS1).
  move=> pc pd; exact: (BZsum_Mlegt0 pd pc).
move /(BZ_lt_diffP pa (BZS_succ pb)); rewrite - (BZdiff_succ_l pb pa) => pc.
apply /(BZ_le_diffP pa pb).
move: (BZp_hi_pr (sub_BZps_BZp pc)).
move: (BZS_diff pb pa); set c := (b -z a) => cz.
move: (BZpred_succ cz) => h pc1.
move: pc; rewrite -/c => /indexed_P [_ pc _].
move: (BZprec_N pc); rewrite pc1 h => ->; apply: BZ_of_natp_i.
by move /setC1_P:pc => [pd pe]; move: (cpred_pr pd pe) => [].
Qed.

Lemma BZ_le_abs n: inc n BZ -> n <=z (BZabs n).
Proof.
move => nz;case /BZ_i0P: (nz).
  move => nn; exact (proj1 (BZ_le_pr2 (BZabs_iN nz) nn)).
by move => np; rewrite (BZabs_pos np); apply:BZ_leR.
Qed.

Lemma BZ_le_triangular n m: inc n BZ -> inc m BZ ->
  (BZabs (n +z m)) <=z (BZabs n) +z (BZabs m).
Proof.
move: n m.
pose aux n m := BZabs (n +z m) <=z BZabs n +z BZabs m.
suff: forall n m, inc n BZp -> inc m BZ -> aux n m.
  move => h n m; case /BZ_i0P; last by apply: h.
  move => pa pb; rewrite - (BZabs_opp) - (BZabs_opp n)- (BZabs_opp m).
  rewrite (BZsum_opp_distr (sub_BZms_BZ pa) pb); apply: h; qprops.
  apply:BZopp_negative2; qprops.
move => n m np; case /BZ_i0P; last first.
  move => mp; rewrite /aux (BZabs_pos np) (BZabs_pos mp).
  move:(BZpS_sum np mp) => pa; move: (sub_BZp_BZ pa) => pb.
  rewrite (BZabs_pos pa); apply: (BZ_leR pb).
move => mn.
move: (sub_BZp_BZ np) (sub_BZms_BZ mn) => nz mz.
move: (BZ_pr1 nz) (BZ_pr1 mz) => pn pm.
rewrite /aux (BZabs_pos np) (BZabs_neg mn).
have [re1 _]: n<z n +z BZopp m.
  by move: (BZ_sum_Mps nz (BZopp_negative1 mn)).
have re2: BZopp m <=z n +z BZopp m.
  rewrite BZsumC; exact(BZ_sum_Mp (BZSo mz) np).
case: (card_le_to_el (CS_Bnat pm) (CS_Bnat pn)) => ce1.
   rewrite (BZsum_pm1 np mn ce1); move: (cdiff_le_symmetry ce1).
   set k := P n -c P m => ce2; rewrite /BZabs /BZ_of_nat; aw.
   have kz: inc (J k C1) BZp by apply: indexed_pi => //;rewrite /k;fprops.
   have le2: