# 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.

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.
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 {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: