Library sset10b
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
Ltac qprops := auto with qprops.
Ltac qw := autorewrite with qw.
We define 0 and the injections N -> Zp and N -> Zm
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.
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
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.
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
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.
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.
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: P (J k C1) <=c P n by aw.
move/ (BZ_le_P1 kz np): le2 => le3; BZo_tac.
rewrite (BZsum_pm2 np mn ce1); move: (cdiff_le_symmetry (proj1 ce1)).
move: (cdiff_nz ce1); set k := P m -c P n => knz ce2.
rewrite /BZabs /BZm_of_nat; Ytac0; aw.
have kz: inc (J k C1) BZp by apply: indexed_pi => //;rewrite /k;fprops.
have le2: P (J k C1) <=c P (BZopp m) by rewrite BZopp_pr1; aw.
move: (sub_BZps_BZp (BZopp_negative1 mn)) => omp.
move / (BZ_le_P1 kz omp): le2 => le3; BZo_tac.
Qed.
Lemma BZ_order_isomorphism_P f:
(order_isomorphism f BZ_ordering BZ_ordering) <->
(exists2 u, inc u BZ & f = Lf (fun z => BZsum z u) BZ BZ).
Proof.
pose p a := Lf (fun z => z +z a) BZ BZ.
have Ha: forall a, inc a BZ -> lf_axiom (fun z => z +z a) BZ BZ.
by move => a az t tz; apply:BZSs.
have Hb: forall a, inc a BZ -> bijection (p a).
move => a az; apply: lf_bijective; first by apply: Ha.
by move => u v uz vz; apply:(BZsum_reg_r uz vz az).
move => y ye; exists (y -z a); first by qprops.
by rewrite BZsumC BZsum_diff.
have Hc: forall a b c, inc a BZ -> b <=z c -> (Vf (p a) b) <=z (Vf (p a) c).
move => a b c az le1;move: (Ha _ az) => h; move: (le1) => [pa pb _].
by rewrite /p; aw; apply /(BZsum_Mleeq pa pb az).
have Hd: (forall a, inc a BZ -> order_isomorphism (p a)BZ_ordering BZ_ordering).
move => a az.
move: BZor_tor BZor_sr => to1 sor; move: (to1) => [or1 _].
have hh:{inc BZ &, fincr_prop (Lf (BZsum^~ a) BZ BZ) BZ_ordering BZ_ordering}.
move => u v uz vz /= /BZ_le_P cuv; apply /BZ_le_P; apply: Hc az cuv.
apply:(total_order_isomorphism to1 or1 (Hb _ az)); rewrite /p; aw.
split; last by move => [u uz ->]; apply: Hd.
move => [_ _ [bf sf tf] incf].
move: sf tf; rewrite BZor_sr => sf tf.
have He: (forall a b, a <=z b -> (Vf f a) <=z (Vf f b)).
move => a b ab; move: (ab) => [pa pb _]; move:ab; move/BZ_le_P.
by rewrite - sf in pa pb; move /(incf _ _ pa pb) /BZ_le_P.
have Hf: (forall a b, a <z b -> (Vf f a) <z (Vf f b)).
move => a b [pa pb]; split; first by apply: He.
dneg pc; move: (pa) => [xa xb _]; rewrite - sf in xa xb.
exact: (bij_inj bf xa xb pc).
have Sa: forall x, inc x BZ -> Vf f (BZsucc x) = (BZsucc (Vf f x)).
move => x xz.
have pa: inc (Vf f x) BZ by Wtac; fct_tac.
move: (BZS_succ pa); rewrite - tf => pb; move: (bij_surj bf pb) => [m].
rewrite sf;move => mf mv; suff: m = BZsucc x by move => <-.
move: (Hf _ _ (BZ_lt_succ xz)) => le1.
case: (BZ_le_to_el mf (BZS_succ xz))=> le2; last first.
move:(Hf _ _ le2); rewrite mv; move /(BZ_lt_succ1P (proj32_1 le1) pa).
move => le3; BZo_tac.
ex_middle ok; move /(BZ_lt_succ1P mf xz): (conj le2 ok) => le3.
move: (He _ _ le3); rewrite mv => l1; move: (BZ_lt_succ pa) => l2; BZo_tac.
have Sb: forall x, inc x BZ -> Vf f (BZpred x) = (BZpred (Vf f x)).
move => x xz; move: (BZS_pred xz) => pxz.
rewrite -{2} (BZsucc_pred xz) (Sa _ pxz) BZpred_succ // -tf; Wtac; fct_tac.
have fz: inc (Vf f \0z) BZ by rewrite -tf;Wtac;[ fct_tac |rewrite sf; qprops].
ex_tac; rewrite -/(p _); move: (Ha _ fz)(Hb _ fz); set g := p (Vf f \0z).
move => Sc Sd.
apply: function_exten; try fct_tac.
by rewrite /g /p;aw.
by rewrite /g /p;aw.
rewrite sf;move => u usf /=.
apply:(BZ_ind (p:= fun z => Vf f z = Vf g z)) => //.
by rewrite /g /p;aw; qw; qprops.
move => x xb; move: (BZS_succ xb) => sxb.
by rewrite (Sa _ xb); move => ->;rewrite /g /p; aw;rewrite (BZsucc_sum xb fz).
move => x xb; move: (BZS_pred xb) => sxb.
by rewrite (Sb _ xb); move => ->; rewrite /g /p; aw;rewrite (BZpred_sum xb fz).
Qed.
Lemma BZpS_prod a b: inc a BZp -> inc b BZp -> inc (a *z b) BZp.
Proof.
move => az bz; rewrite (BZprod_pp az bz); apply :BZ_of_natp_i.
apply:BZprod_aux; qprops.
Qed.
Lemma BZpsS_prod a b: inc a BZps -> inc b BZps -> inc (a *z b) BZps.
Proof.
move => /BZps_iP [ap anz] /BZps_iP [bp bnz]; apply/BZps_iP ; split.
by apply: BZpS_prod.
apply:BZprod_nz => //; qprops.
Qed.
Lemma BZmsuS_prod a b: inc a BZms -> inc b BZms -> inc (a *z b) BZps.
Proof.
move => az bz;apply/BZps_iP ; split.
rewrite (BZprod_mm az bz); apply :BZ_of_natp_i; apply:BZprod_aux; qprops.
by apply:BZprod_nz; qprops; apply: BZms_nz.
Qed.
Lemma BZmuS_prod a b: inc a BZm -> inc b BZm -> inc (a *z b) BZp.
Proof.
case /setU1_P; last by (move => -> _ ; qw; apply: BZpS0).
move => am;case /setU1_P; last by (move => -> ; qw; apply: BZpS0).
move => bm; move :(BZmsuS_prod am bm) => h; qprops.
Qed.
Lemma BZpmsS_prod a b: inc a BZps -> inc b BZms -> inc (a *z b) BZms.
Proof.
move => az bz; move: (BZps_pr1nz az) (proj1 (BZms_hi_pr bz)) => anz bnz.
move: (BZ_pr1 (sub_BZps_BZ az)) (BZ_pr1 (sub_BZms_BZ bz)) => pa pb.
move /BZps_iP: az =>[ap _]; rewrite (BZprod_pm ap bz); apply: BZm_of_natms_i.
fprops.
by apply cprod2_nz.
Qed.
Lemma BZpmS_prod a b: inc a BZp -> inc b BZm -> inc (a *z b) BZm.
Proof.
have zm: inc \0z BZm by apply /setU1_P; right.
move => az; case /setU1_P; last by move ->; qw;apply: zm.
move => bz; case: (equal_or_not a \0z); first by move => ->; qw;apply: zm.
move => anz; move /BZps_iP: (conj az anz) => sap.
by apply /setU1_P; left; apply: BZpmsS_prod.
Qed.
Lemma BZps_stable_prod1 a b: inc a BZ -> inc b BZ -> inc (a *z b) BZps ->
((inc a BZps <-> inc b BZps) /\ (inc a BZms <-> inc b BZms)).
Proof.
move => az bz.
move:BZ_di_neg_spos => H.
case /BZ_i1P: az; first by move => ->; qw => /BZps_iP [_].
case /BZ_i1P: bz; first by move => -> _; qw => /BZps_iP [_].
move => pa pb pc;split; split => // h; [case: (H _ h pb) | case:(H _ h pa)].
move => pa pb pc;case: (H _ _ pc); exact (BZpmsS_prod pb pa).
case /BZ_i1P: bz; first (by move => -> _; qw => /BZps_iP [_]); move => pa pb pc.
case: (H _ _ pc); rewrite BZprodC; exact (BZpmsS_prod pa pb).
split; split => // h; [case: (H _ pb h) | case: (H _ pa h)].
Qed.
Lemma BZprod_Mlege0 a b c: inc c BZp -> a <=z b -> (a *z c) <=z (b *z c).
Proof.
move => cp ab; move: (ab) => [az bz _]; move: (sub_BZp_BZ cp) => cz.
move /(BZ_le_diffP az bz): ab => p1.
apply/ (BZ_le_diffP (BZSp az cz) (BZSp bz cz)).
by rewrite - BZprod_diff_Dl //;apply:BZpS_prod.
Qed.
Lemma BZprod_Mltgt0 a b c: inc c BZps -> a <z b -> (a *z c) <z (b *z c).
Proof.
move => cp ab; move: (ab) => [[az bz _]_]; move: (sub_BZps_BZ cp) => cz.
move /(BZ_lt_diffP az bz): ab => p1.
apply/(BZ_lt_diffP (BZSp az cz) (BZSp bz cz)).
by rewrite - BZprod_diff_Dl //;apply:BZpsS_prod.
Qed.
Lemma BZprod_Mlele0 a b c: inc c BZm -> a <=z b -> (b *z c) <=z (a *z c).
Proof.
move => cm; move: (BZopp_negative2 cm) => ocp ineq.
move: (BZprod_Mlege0 ocp (BZ_le_opp ineq)).
move: ineq => [az bz _]; move: (sub_BZm_BZ cm) => cz.
rewrite BZprod_opp_opp // BZprod_opp_opp //.
Qed.
Lemma BZprod_Mltlt0 a b c: inc c BZms -> a <z b -> (b *z c) <z (a *z c).
Proof.
move => cm; move: (BZopp_negative1 cm) => ocp ineq.
move: (BZprod_Mltgt0 ocp (BZ_lt_opp ineq)).
move: ineq => [[az bz _] _]; move: (sub_BZms_BZ cm) => cz.
rewrite BZprod_opp_opp // BZprod_opp_opp //.
Qed.
Lemma BZ1_small c: inc c BZps -> \1z <=z c.
Proof.
move => h; move: (sub_BZps_BZ h) BZS1 => pa pb; split => //.
move /indexed_P:h => [_ /setC1_P [pc pd] ->];rewrite /BZ_one /BZ_of_nat;aw.
constructor 3;split => //; apply card_ge1; fprops.
Qed.
Lemma BZprod_Mpp b c: inc b BZp -> inc c BZps -> b <=z (b *z c).
Proof.
move => pa pb.
by move: (BZprod_Mlege0 pa (BZ1_small pb)); qw; qprops; rewrite BZprodC.
Qed.
Lemma BZprod_Mlepp a b c: inc b BZp -> inc c BZps -> a <=z b -> a <=z (b *z c).
Proof.
move => pa pb pc; move: (BZprod_Mpp pa pb) => pd; BZo_tac.
Qed.
Lemma BZprod_Mltpp a b c: inc b BZp -> inc c BZps -> a <z b -> a <z (b *z c).
Proof.
move => pa pb pc; move: (BZprod_Mpp pa pb) => pd; BZo_tac.
Qed.
Lemma BZprod_Mlelege0 a b c d: inc b BZp -> inc c BZp ->
a <=z b -> c <=z d -> (a *z c) <=z (b *z d).
Proof.
move => pa pb pc pd.
move: (BZprod_Mlege0 pb pc) (BZprod_Mlege0 pa pd) => r1.
rewrite (BZprodC c) (BZprodC d) => r2; BZo_tac.
Qed.
Lemma BZprod_Mltltgt0 a b c d: inc b BZps -> inc c BZps ->
a <z b -> c <z d -> (a *z c) <z (b *z d).
Proof.
move => pa pb pc pd.
move: (BZprod_Mltgt0 pb pc) (BZprod_Mltgt0 pa pd) => r1.
rewrite (BZprodC c) (BZprodC d) => r2; BZo_tac.
Qed.
Lemma BZprod_Mltltle0 a b c d: inc a BZp -> inc c BZp ->
a <z b -> c <z d -> (a *z c) <z (b *z d).
Proof.
move => pa pb pc pd.
have H: (forall a b, inc a BZp -> a <z b -> inc b BZps).
move => u v up uv; move: (uv) => [[uz vz _] _].
move/ (BZ_lt_diffP uz vz): uv => pe; move: (BZpsS_sum_r up pe).
by rewrite BZsum_diff.
move: (H _ _ pa pc) (H _ _ pb pd) => bp cp.
case: (equal_or_not c \0z) => cnz.
by rewrite cnz; qw; apply /BZ_positive_P1; apply: BZpsS_prod.
by apply: BZprod_Mltltgt0 => //; apply/ BZps_iP;split.
Qed.
Lemma BZprod_Mlegt0 a b c: inc a BZ -> inc b BZ -> inc c BZps ->
(a <=z b <-> (a *z c) <=z (b *z c)).
Proof.
move => pa pb pc; split; first by apply:BZprod_Mlege0; qprops.
move => h; case: (BZ_le_to_el pa pb) => // h1.
move: (BZprod_Mltgt0 pc h1) => h2; BZo_tac.
Qed.
Lemma BZprod_Mltgt00 a b c: inc a BZ -> inc b BZ -> inc c BZps ->
(a <z b <-> (a *z c) <z (b *z c)).
Proof.
move => pa pb pc; split; first by apply:BZprod_Mltgt0; qprops.
move => h; case: (BZ_le_to_el pb pa) => //.
move /(BZprod_Mlegt0 pb pa pc) => h2; BZo_tac.
Qed.
Definition BZdivision_prop a b q r :=
[/\ a = (b *z q) +z r, r <z (BZabs b) & inc r BZp].
Definition BZquo a b :=
let q:= BZ_of_nat ((P a) %/c (P b)) in
Yo (b = \0z) \0z
(Yo (Q a= C1) (Yo (Q b = C1) q (BZopp q))
(Yo ((P a %%c P b) = \0c) (Yo (Q b = C1) (BZopp q) q)
(Yo (Q b = C1) (BZopp (BZsucc q)) (BZsucc q)))).
Notation "x %/z y" := (BZquo x y) (at level 40).
Definition BZrem a b := a -z b *z (a %/z b).
Definition BZdivides b a :=
[/\ inc a BZ, inc b BZ, b <> \0z & BZrem a b = \0z].
Notation "x %%z y" := (BZrem x y) (at level 40).
Notation "x %|z y" := (BZdivides x y) (at level 40).
Lemma BZquo_pr1 a b (q1:= ((P a) %/c (P b))) (q2 := BZ_of_nat q1):
inc a BZ -> inc b BZ -> [/\ inc q1 Bnat, inc q2 BZp & inc q2 BZ].
Proof.
move => az bz; move: (BS_quo (BZ_pr1 az) (BZ_pr1 bz)) => qb.
by move: (BZ_of_natp_i qb) => pa; move: (sub_BZp_BZ pa) => pb.
Qed.
Lemma BZ_quorem0 a: inc a BZ -> (a %%z \0z = a /\ a %/z \0z = \0z).
Proof.
have pa: a %/z \0z = \0z by rewrite /BZquo; Ytac0.
by rewrite /BZrem pa => az; rewrite /BZdiff;qw.
Qed.
Lemma BZ_quorem00 b: inc b BZ -> (\0z %%z b = \0z /\ \0z %/z b = \0z).
Proof.
move => bz.
case: (equal_or_not b \0z); first by move => ->; apply: (BZ_quorem0 BZS0).
move: BZS0 => zz bnz.
have: \0z %/z b = \0z.
rewrite /BZquo; Ytac0; rewrite BZ0_pr1.
move: (cdivision_of_zero (BZ_pr1 bz)) => [[qa qb ->] ->].
by rewrite -/BZ_zero BZopp_0; Ytac0; Ytac0; Ytac0.
move => h;split => //; rewrite /BZrem h; qw; apply: (BZdiff_diag zz).
Qed.
Lemma BZS_quo a b: inc a BZ -> inc b BZ -> inc (a %/z b) BZ.
Proof.
move => az bz; rewrite /BZquo.
move: (BZquo_pr1 az bz) => [_ _]; set q := BZ_of_nat _ => qz.
move: (BZSo qz) (BZS_succ qz) => oqz sqz.
by Ytac ra; [ qprops | Ytac rb; Ytac rc => //; Ytac rd => //]; apply:BZSo.
Qed.
Lemma BZpS_quo a b: inc a BZp -> inc b BZp -> inc (a %/z b) BZp.
Proof.
move => az bz.
move: (BZquo_pr1 (sub_BZp_BZ az) (sub_BZp_BZ bz)) => [_].
set q := BZ_of_nat _ => qz _.
rewrite /BZquo; Ytac ra; first by apply: BZpS0.
by rewrite (BZp_pr2 az) (BZp_pr2 bz);Ytac0; Ytac0.
Qed.
Lemma BZS_rem a b: inc a BZ -> inc b BZ -> inc (a %%z b) BZ.
Proof.
move => pa pb; move: (BZS_quo pa pb) => pc; rewrite /BZrem; qprops.
Qed.
Lemma BZquo_opp_b a b: inc a BZ -> inc b BZ -> a %/z (BZopp b) = BZopp (a %/z b).
Proof.
move => az bz.
case: (equal_or_not b \0z) => bn0.
by rewrite bn0 BZopp_0 (proj2 (BZ_quorem0 az)) BZopp_0.
have bon0: BZopp b <> \0z by dneg xx; move: (BZopp_K bz); rewrite xx BZopp_0.
rewrite /BZquo; Ytac0; Ytac0; rewrite BZopp_pr1.
move: (BZquo_pr1 az bz) => [_ _]; set q := BZ_of_nat _ => qzp.
move: (BZopp_pr2 bz bn0) => [aux1 aux2].
case: (equal_or_not (Q b) C0) => ha.
rewrite (aux1 ha) ha; Ytac0; Ytac0; Ytac0; Ytac0; Ytac0; Ytac0.
by Ytac hb; Ytac0; [symmetry;apply: BZopp_K | Ytac hc; Ytac0].
case: (BZ_pr2 bz); [ by done | move => bp].
rewrite (aux2 bp); do 6 Ytac0; Ytac pc; Ytac0 => //.
by Ytac pd; Ytac0 => //;rewrite BZopp_K //; apply: BZS_succ.
Qed.
Lemma BZrem_opp_b a b: inc a BZ -> inc b BZ -> a %%z (BZopp b) = a %%z b.
Proof.
move => az bz; rewrite /BZrem (BZquo_opp_b az bz).
by rewrite (BZprod_opp_opp bz (BZS_quo az bz)).
Qed.
Lemma BZquo_div1 a b: inc a BZ -> inc b BZ -> b <> \0z ->
(P a) %%c (P b) = \0c -> a = b *z (a %/z b).
Proof.
move => az bz bnz de; rewrite /BZquo; Ytac0; Ytac0.
move: (BZquo_pr1 az bz) => [_ ]; set q := BZ_of_nat _ => [qzp qz].
have pbz: P b <> \0c by move => h; case: bnz; exact (BZ_0_if_abs0 bz h).
move: (card_division(BZ_pr1 az) (BZ_pr1 bz) pbz)=> [_ _ [aa _]].
have aux: cardinalp (P b *c (P a %/c P b)) by rewrite /card_prod; fprops.
have Pa: P a = P b *c P q by rewrite BZ_of_nat_pr1; move: aa; rewrite de;aw.
case: (BZ_pr2 az) => sa; rewrite sa; Ytac0.
rewrite -(proj2 (BZms_hi_pr (BZms_i az sa))) Pa;case: (BZ_pr2 bz) => sb.
by rewrite sb; Ytac0; rewrite (BZprod_mp (BZms_i bz sb) qzp).
Ytac0; rewrite (BZprod_opp_comm bz qz).
have bps: inc b BZps by apply /BZps_iP; split => //; exact (BZp_i bz sb).
by rewrite (BZprod_mp (BZopp_positive1 bps) qzp) BZopp_pr1.
rewrite - (BZp_hi_pr (BZp_i az sa)) Pa;case:(BZ_pr2 bz) => sb; rewrite sb;Ytac0.
move: (sub_BZps_BZp (BZopp_negative1 (BZms_i bz sb))) => h.
by rewrite (BZprod_opp_comm bz qz) (BZprod_pp h qzp) BZopp_pr1.
by rewrite - (BZprod_pp (BZp_i bz sb) qzp).
Qed.
Lemma BZrem_div1 a b: inc a BZ -> inc b BZ -> b <> \0z ->
(P a) %%c (P b) = \0c -> (a %%z b) = \0z.
Proof.
move => az bz bnz de; rewrite /BZrem {1} (BZquo_div1 az bz bnz de).
exact: (BZdiff_diag (BZSp bz (BZS_quo az bz))).
Qed.
Lemma BZquo_opp_a1 a b: inc a BZ -> inc b BZ -> b <> \0z ->
(P a) %%c (P b) = \0c -> (BZopp a) %/z b = BZopp (a %/z b).
Proof.
move => az bz bnz de.
move: (BZquo_div1 az bz bnz de) => r1.
move: de; rewrite -(BZopp_pr1 a) => de.
move: (BZS_quo az bz) (BZSo az) => qz naz.
move: (BZquo_div1 naz bz bnz de); rewrite {1} r1.
rewrite (BZopp_prod_r bz qz) => e1.
symmetry;apply: (BZprod_reg_l (BZSo qz) (BZS_quo naz bz) bz bnz e1).
Qed.
Lemma BZdivision_opp_a2 a b:
inc a BZ -> inc b BZ -> b <> \0z -> (P a %%c P b) <> \0c ->
( (BZopp a) %%z b <> \0z
/\ (BZopp a) %%z b = (BZabs b) -z (a %%z b)).
Proof.
move => az bz bnz pz; split.
set c := BZopp a; move:(BZSo az) => cz.
rewrite /BZrem => ez.
have ha: inc (BZopp a %/z b) BZ by apply: BZS_quo ; qprops.
move /(BZdiff_diag_rw cz (BZSp bz (BZS_quo cz bz))): ez => h.
move: (f_equal P h); rewrite BZopp_pr1 (BZprod_abs2 bz ha); aw.
move: (BZ_pr1 ha); set q := P _ => qB eq.
by move: (cdivides_pr1 qB (BZ_pr1 bz)) => [_ _]; rewrite - eq.
set c := BZabs b.
suff: BZopp a %%z c = c -z a %%z c.
move => t; case /BZ_i0P: (bz) => bs; last by rewrite - (BZabs_pos bs).
by rewrite - (BZrem_opp_b az bz) -( BZrem_opp_b (BZSo az) bz)- (BZabs_neg bs).
rewrite /BZrem; set q := (a %/z c).
suff: BZopp a %/z c = BZopp (BZsucc q).
have bza: inc c BZ by apply: BZSa.
have qz: inc q BZ by apply: BZS_quo; qprops.
have sq1: inc ((q +z \1z)) BZ by qprops.
move: (BZSp bza qz) => sq2.
move => ->.
rewrite /BZsucc /BZdiff (BZopp_prod_r bza (BZSo sq1)) (BZopp_K sq1).
rewrite (BZopp_diff az sq2) BZsumC (BZsumA bza sq2 (BZSo az)).
by rewrite (BZprod_sumDr bza qz BZS1) (BZprod_1r bza) (BZsumC c).
case: (equal_or_not a \0z) => anz.
case: pz; rewrite anz BZ0_pr1.
by move: (cdivision_of_zero (BZ_pr1 bz)) => [ [_ _ ok] _].
have panz: (P a <> \0c) by move =>h; case: anz; exact (BZ_0_if_abs0 az h).
have cnz: c <> \0z by move => cz; move:(BZabs_0p bz cz).
rewrite /q /BZquo (BZabs_pr2 bz)(BZabs_pr1 b) BZopp_pr1; set q1:= (BZ_of_nat _).
have q1z: inc q1 BZ by apply: BZ_of_nat_i; apply: BS_quo; apply: BZ_pr1; qprops.
move: (BZS_succ q1z) => q2z; move: (BZSo q2z) => q3z.
do 5 Ytac0.
rewrite {1} /BZopp.
case: (equal_or_not (Q a) C0).
move => ->; Ytac0; Ytac0; rewrite /BZ_of_nat; aw; Ytac0.
rewrite (BZsum_opp_distr q3z BZS1) (BZopp_K q2z).
rewrite /BZsucc (BZsumC q1) - {1} (BZdiff_sum BZS1 q1z) //.
move => qna; case: (BZ_pr2 az) => qaa; first by case: qna.
by Ytac0; Ytac0; rewrite /BZm_of_nat; Ytac0; aw; Ytac0.
Qed.
Lemma BZdvd_correct a b: inc a BZ -> inc b BZ -> b <> \0z ->
[/\ inc (a %/z b) BZ, inc (a %%z b) BZp &
(BZdivision_prop a b (a %/z b) (a %%z b))].
Proof.
move => az bz bnz.
pose aux a b := a %%z b <z BZabs b /\ inc (a %%z b) BZp.
suff: aux a b.
move: (BZS_quo az bz) => qz [pa pb]; split => //; split => //.
by rewrite /BZrem (BZsum_diff (BZSp bz qz) az).
have Ha: forall a b, inc a BZp -> inc b BZps -> aux a b.
move => u v up /BZps_iP [vp vnz].
rewrite /aux (BZabs_pos vp) /BZrem.
move: (sub_BZp_BZ vp) (sub_BZp_BZ up) => vz uz.
set q := (u %/z v).
suff: (u <z v *z (q +z \1z) /\ v *z q <=z u).
move => [pa pb].
move: (proj31 pb) => pz.
move:(BZS_diff (proj32 pb) pz) => rz.
split; last by apply /(BZ_le_diffP pz uz).
apply /(BZsum_Mlteq rz vz pz); rewrite BZsumC (BZsum_diff pz uz).
by move: pa; rewrite (BZprod_sumDr vz (BZS_quo uz vz) BZS1) BZsumC; qw.
have: q = u %/z v by done.
rewrite /BZquo (BZp_pr2 up) (BZp_pr2 vp); Ytac0; Ytac0; Ytac0=> ->.
move: (BZ_pr1 (sub_BZp_BZ up)) (BZ_pr1 (sub_BZp_BZ vp)) => pa pb.
have pc: P v <> \0c by move => h; case: vnz; exact (BZ_0_if_abs0 vz h).
move: (card_division pa pb pc).
clear q; set q := (P u %/c P v); set r := (P u %%c P v).
move => [qB rB [dp mp]]; move: (BZ_of_natp_i qB) => qzb.
move /BZps_iP: BZps1 => [bz1p _].
split.
rewrite (BZsum_pp qzb bz1p) /BZ_one !BZ_of_nat_pr1.
rewrite (BZprod_pp vp (BZ_of_natp_i (BS_sum qB BS1))) BZ_of_nat_pr1.
apply /(BZ_lt_P1 up);first by apply: BZ_of_natp_i; fprops.
rewrite BZ_of_nat_pr1 dp cprod_sumDl (cprod1r (CS_Bnat pb)).
rewrite csumC (csumC _ (P v));exact:(csum_Mlteq (BS_prod pb qB) pb mp).
have ppb: inc (P v *c q) Bnat by fprops.
rewrite (BZprod_pp vp (BZ_of_natp_i qB)) BZ_of_nat_pr1.
apply /(BZ_le_P1 _ up); first by apply: BZ_of_natp_i.
by rewrite BZ_of_nat_pr1 dp; apply:(Bsum_M0le ppb rB).
have Hb: forall a b, inc a BZp -> inc b BZ -> b <> \0z -> aux a b.
move => u v => up vp vnz.
case /BZ_i1P: vp; [by done | by move => h; apply: Ha | ].
move => vm; move: (BZopp_negative1 vm) => ovp.
move: (BZrem_opp_b (sub_BZp_BZ up) (sub_BZms_BZ vm)) => e1.
by move: (Ha _ _ up ovp); rewrite /aux e1 BZabs_opp.
case /BZ_i0P: (az); last by move => h;apply: Hb.
move => ams; move: (BZopp_negative1 ams) => oap.
move: (Hb _ _ (sub_BZps_BZp oap) bz bnz) => [pa pb].
case: (equal_or_not ((P a) %%c (P b)) \0c) => de.
move: (BZrem_div1 az bz bnz de) => rz.
rewrite /aux rz;split ; [ exact : (BZabs_positive bz bnz) | apply: BZpS0 ].
move: (BZdivision_opp_a2 az bz bnz de) => [r2 r1].
move: pa pb r2; rewrite /aux r1; set X := _ %%z _; set bb := BZabs b.
have Xp: inc X BZ by apply: BZS_rem.
move: (BZSa bz) => abz.
move => pa pb pc; split.
apply /(BZ_lt_diffP Xp abz); apply /BZps_iP; split => // => e1.
move /(BZ_lt_diffP (BZS_diff abz Xp) abz) : pa.
by rewrite /BZdiff BZopp_diff // BZsum_diff //; move /BZps_iP => [].
Qed.
Lemma BZpS_rem a b: inc a BZ -> inc b BZ -> b <> \0z -> inc (a %%z b) BZp.
Proof.
by move => pa pb pc;move: (BZdvd_correct pa pb pc) => [_ ok _].
Qed.
Hint Resolve BZS_quo BZS_rem BZpS_rem: qprops.
Lemma BZrem_small a b: inc a BZ -> inc b BZ -> b <> \0z ->
(a %%z b) <z (BZabs b).
Proof.
by move => pa pb pc;move: (BZdvd_correct pa pb pc) => [_ _ [ _ bb _]].
Qed.
Lemma BZdvd_exact b q: inc q BZ -> inc b BZ -> b <> \0z ->
((q *z b) %/z b = q /\ (q *z b) %%z b = \0z).
Proof.
move => qz bz bnz; move: (BZSp qz bz);set a := (q *z b) => az.
have aux: (P a) %%c (P b) = \0c.
move: (cdivides_pr1 (BZ_pr1 qz) (BZ_pr1 bz)) => [_ _].
by rewrite BZprod_pr1 cprodC.
split; last by rewrite (BZrem_div1 az bz bnz aux).
move: (BZquo_div1 az bz bnz aux). rewrite {1} /a BZprodC => h.
symmetry; exact (BZprod_reg_l qz (BZS_quo az bz) bz bnz h).
Qed.
Lemma BZdvd_unique a b q r q' r': inc a BZ -> inc b BZ -> b <> \0z ->
inc q BZ -> inc r BZ -> inc q' BZ -> inc r' BZ ->
BZdivision_prop a b q r -> BZdivision_prop a b q' r' ->
(q = q' /\ r =r').
Proof.
move => az bz qnz; move: q r q' r'.
have alt:forall q r, inc q BZ -> inc r BZ -> BZdivision_prop a b q r ->
[/\ (b *z q) <=z a, a <z (b *z ((BZsign b) +z q)) & r = a -z (b *z q)].
move => q r qz rz.
move: (BZSp bz qz) (BZS_sign b) => qa qb.
have qc: b *z (BZsign b +z q) = b *z q +z BZabs b.
by rewrite (BZprod_sumDr bz qb qz) BZsumC (BZsign_abs bz).
move: (BZsum_Meqlt rz (BZSa bz) qa) => qd.
move => [pa pb pc];split => //.
by rewrite pa; apply: BZ_sum_Mp.
by rewrite qc pa; apply /qd.
by rewrite pa BZdiff_sum.
move => q r q' r' qz rz q'z r'z h h'.
move: (alt _ _ qz rz h) => [pa pb pc].
move: (alt _ _ q'z r'z h') => [pa' pb' pc'].
suff: q = q' by move => sq; rewrite pc pc' sq.
move: (BZS_sign b) => ab.
have aux: forall q q', inc q BZ -> inc q' BZ ->
b *z q' <z b *z (BZsign b +z q) -> inc (b *z (BZsign b +z (q -z q'))) BZps.
move => z z' zz z'z le.
move: (BZSs ab zz) => sa.
move /(BZ_lt_diffP (BZSp bz z'z) (BZSp bz sa)): le.
by rewrite - (BZprod_diff_Dr bz sa z'z) /BZdiff (BZsumA ab zz (BZSo z'z)).
have aux2: forall q q', inc q BZ -> inc q' BZ ->
inc (\1z +z (q -z q')) BZps -> q' <=z q.
move => z z' zz z'z le;apply /(BZ_lt_succ1P z'z zz).
apply /(BZ_lt_diffP z'z (BZS_succ zz)).
rewrite /BZsucc /BZdiff (BZsumC z) - BZsumA //; qprops.
have aux3: forall q q', inc q BZ -> inc q' BZ ->
inc (\1mz +z (q -z q')) BZms -> q <=z q'.
move => z z' zz z'z le; move: (BZopp_negative1 le).
rewrite (BZsum_opp_distr BZSm1 (BZS_diff zz z'z)).
by rewrite (BZopp_diff zz z'z) BZopp_m1; apply: aux2.
have r1: b *z q <z b *z (BZsign b +z q') by BZo_tac.
have r2: b *z q' <z b *z (BZsign b +z q) by BZo_tac.
move: (aux _ _ qz q'z r2) (aux _ _ q'z qz r1) => r3 r4.
move: (BZps_stable_prod1 bz (BZSs ab (BZS_diff qz q'z)) r3).
move: (BZps_stable_prod1 bz (BZSs ab (BZS_diff q'z qz)) r4).
case /BZ_i1P: bz => ha //.
move=> [s1 s2] [s3 s4].
move/s1: (ha); move/s3: (ha); rewrite (BZsign_pos ha) => s5 s6.
move: (aux2 _ _ qz q'z s5) (aux2 _ _ q'z qz s6) => l1 l2; BZo_tac.
move=> [s1 s2] [s3 s4].
move/s2: (ha); move/s4: (ha); rewrite (BZsign_neg ha) => s5 s6.
move: (aux3 _ _ qz q'z s5) (aux3 _ _ q'z qz s6) => l1 l2; BZo_tac.
Qed.
Lemma BZdvd_unique1 a b q r: inc a BZ -> inc b BZ ->
inc q BZ -> inc r BZ -> b <> \0z ->
BZdivision_prop a b q r -> (q = a %/z b /\ r = a %%z b).
Proof.
move => pa pb pc pd pe H1.
move: (BZdvd_correct pa pb pe) => [pc' pd'' H2].
exact (BZdvd_unique pa pb pe pc pd pc' (sub_BZp_BZ pd'') H1 H2).
Qed.
Lemma BZdvds_pr a b: b %|z a -> a = b *z (a %/z b).
Proof.
move => [pa pb pc pd].
move: pd; rewrite /BZrem => h.
exact (BZdiff_diag_rw pa (BZSp pb (BZS_quo pa pb)) h).
Qed.
Lemma BZdvds_pr1 a b: inc a BZ -> inc b BZ -> b <> \0z -> b %|z (a *z b).
Proof.
move => pa pb pc; move:(BZdvd_exact pa pb pc) => [_ dd].
split => //; qprops.
Qed.
Lemma BZdvds_pr1' a b: inc a BZ -> inc b BZ -> b <> \0z -> b %|z (b *z a).
Proof. by move => pa pb pc; rewrite BZprodC; apply:BZdvds_pr1. Qed.
Lemma BZdvd_pr2 a b q: inc q BZ -> inc b BZ -> b <> \0z ->
a = b *z q -> q = a %/z b.
Proof.
move => qz bz bnz pd.
move: (BZSp bz qz); rewrite - pd => az.
have hh: (BZdivision_prop a b q \0z).
red; rewrite - pd (BZsum_0r az);split => //; last by apply: BZpS0.
split; last by move => abz; case: bnz;apply: (BZabs_0p bz).
apply /BZ_positive_P; exact (BZabs_iN bz).
exact (proj1 (BZdvd_unique1 az bz qz BZS0 bnz hh)).
Qed.
Lemma BZdvds_pr0 a b: b %|z a -> (P b) %|c (P a).
Proof.
move => [az bz bnz etc].
move: (BZdiff_diag_rw az (BZSp bz (BZS_quo az bz)) etc).
move => h; move: (f_equal P h); rewrite BZprod_pr1 => ->.
apply: cdivides_pr1; apply: BZ_pr1 => //; qprops.
Qed.
Lemma BZdvds_pr3 a b: inc a BZ -> inc b BZ -> b <> \0z ->
(b %|z a <-> (P b) %|c (P a)).
Proof.
move => az bz bnz.
split; first by apply:BZdvds_pr0.
move => [sa sb sc]; split => //; exact:(BZrem_div1 az bz bnz sc).
Qed.
Lemma BZdvds_opp1 a b: inc b BZ ->
(b %|z a <-> (BZopp b) %|z a).
Proof.
move => bz; move: (BZSo bz) => obz.
split;move=> [pa pb pc]; rewrite /BZdivides (BZrem_opp_b pa bz).
by move => h;split => //; apply /(BZnon_zero_opp bz).
by move => h;split => //; apply /(BZnon_zero_opp bz).
Qed.
Lemma BZdvds_opp2 a b: inc a BZ -> (b %|z a <-> b %|z (BZopp a)).
Proof.
move => az; move: (BZSo az) => oaz.
split; move => h; move: (BZdvds_pr0 h) => h1;move: h=> [pa pb pc _].
by apply /(BZdvds_pr3 oaz pb pc); rewrite BZopp_pr1.
by apply /(BZdvds_pr3 az pb pc); rewrite -(BZopp_pr1 a).
Qed.
Lemma BZquo_opp2 a b: b %|z a -> (BZopp a) %/z b = BZopp (a %/z b).
Proof.
move => h; move: (BZdvds_pr0 h) => [_ _ h1].
by move: h => [pa pb pc pd]; apply: BZquo_opp_a1.
Qed.
Lemma BZdvds_one a: inc a BZ -> \1z %|z a.
Proof. by move=> az; move: (BZdvds_pr1 az BZS1 BZ_one_not_zero); qw. Qed.
Lemma BZdvds_mone a: inc a BZ -> \1mz %|z a.
Proof.
by move=> az;rewrite - BZopp_1; move/(BZdvds_opp1 a BZS1) : (BZdvds_one az).
Qed.
Lemma BZquo_one a: inc a BZ -> a %/z \1z = a.
Proof.
by move => az; symmetry; apply:(BZdvd_pr2 az BZS1 BZ_one_not_zero); qw.
Qed.
Lemma BZquo_mone a: inc a BZ -> a %/z \1mz = BZopp a.
Proof.
move=> az;rewrite - BZopp_1 - {2} (BZquo_one az); apply:BZquo_opp_b; qprops.
Qed.
Lemma BZdvds_pr4 a b q: b %|z a -> q = a %/z b -> a = b *z q.
Proof. by move => H ->;exact: (BZdvds_pr H). Qed.
Lemma BZdvds_pr5 b q: inc b BZ -> inc q BZ -> b <> \0z -> (b *z q) %/z b = q.
Proof. by move=> pa pb pc; symmetry; apply:BZdvd_pr2. Qed.
Lemma BZdvd_itself a: inc a BZ -> a <> \0z -> (a %|z a /\ a %/z a = \1z).
Proof.
move => az anz.
by move: (BZdvds_pr1 BZS1 az anz) (BZdvds_pr5 az BZS1 anz); qw.
Qed.
Lemma BZdvd_opp a: inc a BZ -> a <> \0z ->
(a %|z (BZopp a) /\ (BZopp a) %/z a = \1mz).
Proof.
move => az anz;move: (BZdvd_itself az anz) => [pa pb].
by rewrite (BZquo_opp2 pa) pb BZopp_1;split => //; apply/ (BZdvds_opp2 a az).
Qed.
Lemma BZdvd_zero1 a: inc a BZ -> a <> \0z -> (a %|z \0z /\ \0z %/z a = \0z).
Proof.
move => az anz; move: (BZ_quorem00 az) => [pa pb].
split => //; split => //; qprops.
Qed.
Lemma BZdvds_trans a b a': a %|z a'-> b %|z a -> b %|z a'.
Proof.
move => pa pb.
rewrite (BZdvds_pr pa) {1} (BZdvds_pr pb).
move: pa pb => [a'z az _ _] [_ bz bnz _].
move: (BZS_quo az bz)(BZS_quo a'z az) => qa qb.
rewrite - (BZprodA bz qa qb) BZprodC.
by apply: (BZdvds_pr1 (BZSp qa qb) bz bnz).
Qed.
Lemma BZdvds_trans1 a b a': a %|z a'-> b %|z a ->
a' %/z b = (a' %/z a) *z (a %/z b).
Proof.
move => pa pb.
rewrite {1} (BZdvds_pr pa) {1} (BZdvds_pr pb).
move: pa pb => [a'z az _ _ ] [_ bz bnz _].
move: (BZS_quo az bz)(BZS_quo a'z az) => qa qb.
by rewrite - (BZprodA bz qa qb) (BZdvds_pr5 bz (BZSp qa qb) bnz) BZprodC.
Qed.
Lemma BZdvds_trans2 a b c: inc c BZ -> b %|z a -> b %|z (c *z a).
Proof.
move => cz dv1.
case: (equal_or_not a \0z) => anz.
by move: dv1;rewrite anz; qw.
move: (dv1)=> [h _ _ _].
exact: (BZdvds_trans (BZdvds_pr1 cz h anz) dv1).
Qed.
Lemma BZquo_simplify a b c: inc a BZ -> inc b BZ -> inc c BZps ->
b <> \0z ->
( (a *z c) %/z(b *z c) = a %/z b /\
(a *z c) %%z (b *z c) = (a %%z b) *z c).
Proof.
move => az bz czp bnz.
move:(BZdvd_correct az bz bnz); set q := a %/z b; set r := (a %%z b).
move => [qz rzp [qr r0 r1]].
move: (sub_BZps_BZ czp)(sub_BZp_BZ rzp) => cz rz.
move /BZps_iP: (czp) => [pa pb].
move: (BZpS_prod rzp pa) => pc.
have pd: a *z c = (b *z c) *z q +z r *z c.
rewrite qr (BZprod_sumDl cz (BZSp bz qz) rz).
by rewrite BZprodC (BZprodA cz bz qz) (BZprodC c).
have pe: r *z c <z BZabs (b *z c).
rewrite (BZprod_abs bz cz) (BZabs_pos pa).
by apply /(BZprod_Mltgt00 rz (BZSa bz) czp).
have bcnz: (b *z c) <> \0z.
by apply: BZprod_nz => //;move /BZps_iP: czp => [_].
have h: (BZdivision_prop (a *z c) (b *z c) q (r *z c)) by split => //.
move: (BZdvd_unique1 (BZSp az cz) (BZSp bz cz) qz (BZSp rz cz) bcnz h).
by move => [-> ->].
Qed.
Lemma BZdvds_prod a b c: inc a BZ -> inc b BZ -> inc c BZ -> c <> \0z ->
( a %|z b <-> (a *z c) %|z (b *z c)).
Proof.
move => az bz cz cnz.
move: (BZS_quo bz az) => baz.
split => h.
rewrite (BZdvds_pr h) (BZprodC a (b %/z a)) -(BZprodA baz az cz).
apply:(BZdvds_pr1 baz (BZSp az cz)); apply: BZprod_nz => //.
by move: h => [_ _ ].
move: (BZdvds_pr h).
move: (BZS_quo (BZSp bz cz)(BZSp az cz)).
set t := (b *z c) %/z (a *z c) => tz.
rewrite (BZprodC a) (BZprodC _ c) - (BZprodA cz az tz) => h1.
rewrite (BZprod_reg_l bz (BZSp az tz) cz cnz h1) BZprodC.
apply:(BZdvds_pr1 tz az) => aez; move: h => [_ _ acnz _].
by case: acnz; rewrite aez; qw.
Qed.
Lemma BZdvd_and_sum a a' b: b %|z a -> b %|z a'
-> ( b %|z (a +z a') /\ (a +z a') %/z b = (a %/z b) +z (a' %/z b)).
Proof.
move => pa pb; move: (BZdvds_pr pa) (BZdvds_pr pb).
set q1 := a %/z b; set q2:= a' %/z b => e1 e2.
move: pa pb => [az bz bnz _] [a'z _ _ _].
move: (BZS_quo az bz)(BZS_quo a'z bz) => q1z q2z.
have -> : a +z a' = b *z (q1 +z q2).
by rewrite e1 e2 (BZprod_sumDr bz q1z q2z).
rewrite (BZdvds_pr5 bz (BZSs q1z q2z) bnz);split => //.
rewrite BZprodC;apply: (BZdvds_pr1 (BZSs q1z q2z) bz bnz).
Qed.
Lemma BZdvd_and_diff a a' b: b %|z a -> b %|z a'
-> ( b %|z (a -z a') /\ (a -z a') %/z b = (a %/z b) -z (a' %/z b)).
Proof.
move => h1 h2; rewrite /BZdiff.
move:(h2) => [a'z _ _ _].
rewrite - (BZquo_opp2 h2).
move /(BZdvds_opp2 _ a'z): h2 => h3.
exact (BZdvd_and_sum h1 h3).
Qed.
Definition BZ_ideal x:=
[/\ (forall a, inc a x -> inc a BZ),
(forall a b, inc a x -> inc b x -> inc (a +z b) x) &
(forall a b, inc a x -> inc b BZ -> inc (a *z b) x)].
Definition BZ_ideal2 a b := Zo BZ (fun z =>
exists u v, [/\ inc u BZ, inc v BZ & z = (a *z u) +z (b *z v)]).
Lemma BZ_in_ideal1 a b: inc a BZ -> inc b BZ ->
(inc a (BZ_ideal2 a b) /\ inc b (BZ_ideal2 a b)).
Proof.
move => az bz; split; apply /Zo_P;split => //.
exists \1z; exists \0z;qw=> //; split; qprops.
exists \0z; exists \1z;qw => //; split;qprops.
Qed.
Lemma BZ_is_ideal2 a b: inc a BZ -> inc b BZ -> BZ_ideal (BZ_ideal2 a b).
Proof.
move => az bz.
split; first by move => x /Zo_P [].
move => x y /Zo_P [xz [u [v [uz vz pa]]]] /Zo_P [yz [w [z [wz zz pb]]]].
apply /Zo_P; split; first by apply:BZSs.
exists (u +z w); exists (v +z z); split; [qprops | qprops | ].
rewrite (BZprod_sumDr az uz wz) (BZprod_sumDr bz vz zz).
rewrite BZsum_permute_2_in_4; first (by rewrite -pa -pb);by apply: BZSp.
move => x y /Zo_P [xz [u [v [uz vz pa]]]] yz.
apply /Zo_P; split; first by apply:BZSp.
exists (u *z y); exists (v *z y); split; [qprops | qprops | ].
rewrite (BZprodA az uz yz) (BZprodA bz vz yz).
by rewrite - (BZprod_sumDl yz (BZSp az uz) (BZSp bz vz)) -pa.
Qed.
Definition BZ_ideal1 a := fun_image BZ (fun z => a *z z).
Lemma BZ_in_ideal3 a: inc a BZ -> BZ_ideal1 a = BZ_ideal2 a a.
Proof.
move => az; set_extens t.
move /funI_P => [x xz ->]; apply /Zo_P; split; first by qprops.
exists x; exists \0z;split => //; [ qprops | qw; qprops].
move=> /Zo_P [xz [u [v [uz vz pa]]]]; apply /funI_P.
by exists (u +z v);[ qprops | rewrite (BZprod_sumDr az uz vz) pa].
Qed.
Lemma BZ_in_ideal4 a: inc a BZ ->
(BZ_ideal (BZ_ideal1 a) /\ inc a (BZ_ideal1 a)).
Proof.
move=> az; rewrite (BZ_in_ideal3 az); split; first by apply: BZ_is_ideal2.
apply: (proj1 (BZ_in_ideal1 az az)).
Qed.
Lemma BZ_idealS_opp a x: BZ_ideal x -> inc a x -> inc (BZopp a) x.
Proof.
move => [pa _ pb] ax; rewrite - (BZprod_m1r (pa _ ax)).
exact: (pb _ _ ax BZSm1).
Qed.
Lemma BZ_idealS_abs a x: BZ_ideal x -> inc a x -> inc (BZabs a) x.
Proof.
move => pa pb.
case /BZ_i0P: (proj31 pa _ pb) => az; last by rewrite (BZabs_pos az).
by rewrite (BZabs_neg az); apply: BZ_idealS_opp.
Qed.
Lemma BZ_idealS_diff a b x:
BZ_ideal x -> inc a x -> inc b x -> inc (a -z b) x.
Proof.
move => ix ax bx; rewrite /BZdiff.
apply (proj32 ix _ _ ax (BZ_idealS_opp ix bx)).
Qed.
Lemma BZ_idealS_rem a b x: BZ_ideal x -> inc a x -> inc b x -> inc (a %%z b) x.
Proof.
move => ix ax bx; rewrite /BZrem; apply: (BZ_idealS_diff ix ax).
exact: (proj33 ix _ _ bx (BZS_quo (proj31 ix _ ax) (proj31 ix _ bx))).
Qed.
Lemma BZ_ideal_0P a: inc a (BZ_ideal1 \0z) <-> (a = \0z).
Proof.
split.
by move => /funI_P [z]; qw; move => _.
move => az; apply /funI_P; exists \0z; qw;qprops.
Qed.
Lemma BZ_N_worder X: sub X BZp -> nonempty X ->
exists2 a, inc a X & forall b, inc b X -> BZ_le a b.
Proof.
move => pa [t tx];set (Y:= fun_image X P).
have yb: sub Y Bnat.
move => y /funI_P [z zz ->]; apply: (BZ_pr1 (sub_BZp_BZ (pa _ zz))).
have ney: (nonempty Y) by exists (P t); apply /funI_P; ex_tac.
move: (Bnat_order_wor) => [[or wor] sr].
have yb1: sub Y (substrate Bnat_order) by rewrite sr.
move: (wor _ yb1 ney) => [y []]; aw => yy aux.
move /funI_P: (yy) => [z zx pz]; ex_tac.
move => b bx; apply /(BZ_le_P1 (pa _ zx) (pa _ bx)); rewrite - pz.
have pby: inc (P b) Y by apply /funI_P; ex_tac.
by move: (iorder_gle1 (aux _ pby)) => /Bnat_order_leP [_ _].
Qed.
Theorem BZ_principal x: BZ_ideal x -> nonempty x ->
exists2 a, inc a BZp & BZ_ideal1 a = x.
Proof.
move => ix nex.
case: (p_or_not_p (exists2 a, inc a x & a <> \0z)); last first.
move => h; exists \0z; first by apply: BZpS0.
set_extens t.
move:nex => [q qx]; move: (proj33 ix _ _ qx BZS0); qw => x0.
move /BZ_ideal_0P => tx; ue.
move => tx; apply /BZ_ideal_0P; ex_middle xnz; case: h;ex_tac.
move=> [a ax anz].
set (Z:= BZps \cap x).
have pa: sub Z BZp by move => t /setI2_P [ta _]; apply: sub_BZps_BZp.
have pb: nonempty Z.
exists (BZabs a); apply/setI2_P; split; last by apply:BZ_idealS_abs.
apply /BZ_positive_P1; exact: (BZabs_positive (proj31 ix _ ax) anz).
move: (BZ_N_worder pa pb) => [b bz bm].
move /setI2_P: bz => [] /BZps_iP [bzp bnz] bx; ex_tac.
move: (sub_BZp_BZ bzp) => bz.
set_extens t.
move/funI_P => [u uz ->]; apply: (proj33 ix _ _ bx uz).
move => tx.
move: (BZ_idealS_rem ix tx bx) => rx.
move: (BZdvd_correct (proj31 ix _ tx) bz bnz).
move => [qa qb [qc qd qe]].
case: (equal_or_not (t %%z b) \0z) => tnz.
move: (BZSp bz qa) => pz.
rewrite qc tnz (BZsum_0r pz); apply /funI_P; exists (t %/z b) => //.
have rz: inc (t %%z b) Z by apply /setI2_P; split => //; apply /BZps_iP.
move:qd (bm _ rz);rewrite (BZabs_pos bzp) => la lb; BZo_tac.
Qed.
Lemma BZ_ideal_unique_gen a b: inc a BZ -> inc b BZ ->
BZ_ideal1 a = BZ_ideal1 b -> BZabs a = BZabs b.
Proof.
move => az bz sv.
move: (BZ_in_ideal4 az) (BZ_in_ideal4 bz) => [pa pb] [_].
rewrite - sv => /funI_P [z zz eq1].
move: pb; rewrite sv => /funI_P [u uz]; rewrite eq1.
rewrite - (BZprodA az zz uz) => aux.
move: (BZprod_abs az zz); rewrite - eq1;move => ->.
move: (BZSa az) => aaz.
by case: (BZprod_1_inversion_more az zz uz aux);
move => ->; rewrite? BZabs_1 ?BZabs_m1; qw.
Qed.
Lemma BZ_ideal_unique_gen1 a b: inc a BZp -> inc b BZp ->
BZ_ideal1 a = BZ_ideal1 b -> a = b.
Proof.
move => pa pb pc; move:(BZ_ideal_unique_gen (sub_BZp_BZ pa) (sub_BZp_BZ pb) pc).
by rewrite (BZabs_pos pa) (BZabs_pos pb).
Qed.
Definition BZgcd a b := select (fun z => BZ_ideal1 z = BZ_ideal2 a b) BZp.
Definition BZlcm a b := (a *z b) %/z (BZgcd a b).
Definition BZ_coprime a b := BZgcd a b = \1z.
Lemma BZgcd_prop1 a b: inc a BZ -> inc b BZ ->
(inc (BZgcd a b) BZp /\ BZ_ideal1 (BZgcd a b) = BZ_ideal2 a b).
Proof.
move => az bz.
set p := (fun z => BZ_ideal1 z = BZ_ideal2 a b).
have pa: singl_val2 (inc^~ BZp) p.
rewrite /p;move => x y /= pa e1 pb e2;apply: (BZ_ideal_unique_gen1 pa pb); ue.
move:(BZ_is_ideal2 az bz)=> idax.
have neid: nonempty (BZ_ideal2 a b).
move: (proj1 (BZ_in_ideal1 az bz)) => pb; ex_tac.
move: (BZ_principal idax neid) => [c ca cb].
move: (select_uniq pa ca cb). rewrite /p -/(BZgcd a b) => <-;split => //.
Qed.
Lemma BZpS_gcd a b: inc a BZ -> inc b BZ -> inc (BZgcd a b) BZp.
Proof. move => az bz; exact: (proj1(BZgcd_prop1 az bz)). Qed.
Lemma BZS_gcd a b: inc a BZ -> inc b BZ -> inc (BZgcd a b) BZ.
Proof. move => az bz; move: (BZpS_gcd az bz) => h; qprops. Qed.
Lemma BZ_gcd_unq a b g: inc a BZ -> inc b BZ ->
inc g BZp -> BZ_ideal1 g = BZ_ideal2 a b ->
g = (BZgcd a b).
Proof.
move => az bz gp idp.
set p := (fun z => BZ_ideal1 z = BZ_ideal2 a b).
have un: (forall x y, inc x BZp -> inc y BZp -> p x -> p y -> x = y).
rewrite /p;move => x y pa pb e1 e2; apply: (BZ_ideal_unique_gen1 pa pb); ue.
move:(BZgcd_prop1 az bz) => [pa pb].
exact (un _ _ gp pa idp pb).
Qed.
Hint Resolve BZpS_gcd : qprops.
Lemma BZgcd_div a b (g:= (BZgcd a b)): inc a BZ -> inc b BZ ->
a = g *z (a %/z g) /\ b = g *z (b %/z g).
Proof.
move => az bz; move: (BZgcd_prop1 az bz)=> [pa pb].
move: (BZ_in_ideal1 az bz); rewrite - pb -/g.
move => [] /funI_P [q qa qb] /funI_P [q' qa' qb'].
case:(equal_or_not g \0z) => qnz; first by rewrite {1} qb {1} qb' qnz; qw.
move: (sub_BZp_BZ pa) => pc.
split.
apply: BZdvds_pr; rewrite qb; rewrite BZprodC;apply: (BZdvds_pr1 qa pc qnz).
apply: BZdvds_pr; rewrite qb'; rewrite BZprodC;apply: (BZdvds_pr1 qa' pc qnz).
Qed.
Lemma BZgcd_nz a b: inc a BZ -> inc b BZ ->
BZgcd a b = \0z -> (a = \0z /\ b = \0z).
Proof.
by move => az bz h; move: (BZgcd_div az bz); rewrite h; qw.
Qed.
Lemma BZgcd_nz1 a b: inc a BZ -> inc b BZ ->
(a <> \0z \/ b <> \0z) -> BZgcd a b <> \0z.
Proof.
by move => az bz h gnz; move: (BZgcd_nz az bz gnz) => [a0 b0]; case: h.
Qed.
Lemma BZ_nz_quo_gcd a b: inc a BZ -> inc b BZ -> a <> \0z ->
a %/z (BZgcd a b) <> \0z.
Proof.
by move => az bz anz qz; move: (proj1 (BZgcd_div az bz)); rewrite qz; qw.
Qed.
Lemma BZ_positive_quo_gcd a b: inc a BZp -> inc b BZ ->
inc (a %/z (BZgcd a b)) BZp.
Proof. move => azp bz; apply:BZpS_quo; qprops. Qed.
Lemma BZgcd_prop2 a b: inc a BZ -> inc b BZ ->
(exists x y, [/\ inc x BZ, inc y BZ &
(BZgcd a b = (a *z x) +z (b *z y))]).
Proof.
move => az bz; move: (BZgcd_prop1 az bz) => [pa pb].
by move: (BZ_in_ideal4 (sub_BZp_BZ pa)) => [_]; rewrite pb => /Zo_P [_].
Qed.
Lemma BZgcd_C a b: BZgcd a b = BZgcd b a.
Proof.
suff: BZ_ideal2 a b = BZ_ideal2 b a by rewrite /BZgcd => ->.
by set_extens t => /Zo_P [pa [u [v [uc vz etc]]]]; apply:Zo_i => //;
exists v ;exists u; rewrite BZsumC.
Qed.
Lemma BZgcd_opp a b: inc a BZ -> inc b BZ -> BZgcd a b = BZgcd (BZopp a) b.
Proof.
move => az bz.
suff: BZ_ideal2 a b = BZ_ideal2 (BZopp a) b by rewrite /BZgcd => ->.
set_extens t => /Zo_P [pa [u [v [uc vz etc]]]]; apply:Zo_i => //;
exists (BZopp u) ;exists v;split => //;qprops.
by rewrite BZprod_opp_opp.
by rewrite BZprod_opp_comm.
Qed.
Lemma BZ_gcd_abs a b: inc a BZ -> inc b BZ ->
BZgcd a b = BZgcd (BZabs a) (BZabs b).
Proof.
have h:(forall a b, inc a BZ -> inc b BZ -> BZgcd a b = BZgcd (BZabs a) b).
move => u v uz vz; case /BZ_i0P: (uz) => su.
by rewrite (BZabs_neg su) (BZgcd_opp uz vz).
by rewrite (BZabs_pos su).
by move => az bz; rewrite (h _ _ az bz) BZgcd_C (h _ _ bz (BZSa az)) BZgcd_C.
Qed.
Lemma BZgcd_id a: inc a BZ -> BZgcd a a = BZabs a.
Proof.
move => az; rewrite (BZ_gcd_abs az az); set b := BZabs a.
move: (BZabs_iN az) => bzp; move: (sub_BZp_BZ bzp) => bz.
by rewrite - (BZ_gcd_unq bz bz bzp (BZ_in_ideal3 bz)).
Qed.
Lemma BZgcd_rem a b q: inc a BZ -> inc b BZ -> inc q BZ ->
BZgcd a (b +z a *z q) = BZgcd a b.
Proof.
move => az bz qz.
suff: BZ_ideal2 a b = BZ_ideal2 a (b +z a *z q) by rewrite /BZgcd => ->.
move: (BZSp az qz) => aqz.
set_extens t => /Zo_P [pa [u [v [uz vz etc]]]]; apply:Zo_i => //.
move:(BZSp vz qz) => vqz; move: (BZS_diff uz vqz)=> ha.
exists (u -z v *z q); exists v;split => //.
move: (BZSp aqz vz)=> pa1.
rewrite (BZprod_diff_Dr az uz vqz) (BZprod_sumDl vz bz aqz).
rewrite (BZprodC v) (BZprodA az qz vz).
rewrite (BZsum_permute_2_in_4 (BZSp az uz)(BZSo pa1) (BZSp bz vz) pa1) - etc.
by rewrite (BZsumC _ ((a *z q) *z v)) - /(_ -z _) (BZdiff_diag pa1); qw.
move : etc; rewrite (BZprod_sumDl vz bz aqz) (BZsumC (b *z v)).
rewrite (BZsumA (BZSp az uz) (BZSp aqz vz) (BZSp bz vz)) - (BZprodA az qz vz).
move: (BZSp qz vz) => qvz.
rewrite -(BZprod_sumDr az uz qvz) => ->.
exists (u +z q *z v); exists v; split => //; qprops.
Qed.
Lemma BZgcd_diff a b: inc a BZ -> inc b BZ -> BZgcd a (b -z a) = BZgcd a b.
Proof.
move => az bz; move: (BZgcd_rem az bz BZSm1).
by rewrite (BZprod_m1r az).
Qed.
Lemma BZgcd_zero a: inc a BZ -> BZgcd a \0z = BZabs a.
Proof.
by move => az; move:(BZgcd_diff az az); rewrite (BZdiff_diag az) (BZgcd_id az).
Qed.
Lemma BZS_lcm a b: inc a BZ -> inc b BZ -> inc (BZlcm a b) BZ.
Proof.
move => az bz; move: (BZS_gcd az bz) => gz.
apply: (BZS_quo (BZSp az bz) gz).
Qed.
Lemma BZlcm_zero a: inc a BZ -> BZlcm a \0z = \0z.
Proof.
move => az. rewrite /BZlcm. qw.
exact (proj2 (BZ_quorem00 (sub_BZp_BZ (BZpS_gcd az BZS0)))).
Qed.
Lemma BZlcm_prop1 a b (g := BZgcd a b) (l := BZlcm a b):
inc a BZ -> inc b BZ ->
[/\ l = (a %/z g) *z b, l = a *z (b %/z g) &
l = ((a %/z g) *z (b %/z g)) *z g].
Proof.
move => az bz.
move: (BZS_gcd az bz) => gz.
case:(equal_or_not b \0z) => bnz.
rewrite /l bnz (BZlcm_zero az); qw.
rewrite (proj2 (BZ_quorem00 gz)); qw;split => //.
move: (BZgcd_div az bz); rewrite -/g.
set q1:= (a %/z g); set q2 := (b %/z g); move => [pa pb].
move: (BZS_quo az gz) (BZS_quo bz gz) => q1z q2z.
suff: l = q1 *z b.
move => ->;split => //; rewrite pb ? pa.
by rewrite (BZprodA q1z gz q2z) (BZprodC g _).
by rewrite (BZprodC g _) (BZprodA q1z q2z gz).
rewrite/l/BZlcm{1} pa -(BZprodA gz q1z bz); apply:(BZdvds_pr5 gz (BZSp q1z bz)).
by apply: (BZgcd_nz1 az bz); right.
Qed.
Lemma BZlcm_nonzero a b: inc a BZ -> inc b BZ ->
a <> \0z -> b <> \0z -> BZlcm a b <> \0z.
Proof.
move=> az bz ane bnz.
move: (sub_BZp_BZ(BZpS_gcd az bz)) => gz.
move: (BZlcm_prop1 az bz).
set u := (a %/z BZgcd a b); move => [h _ _]; rewrite h.
apply:(BZprod_nz (BZS_quo az gz) bz _ bnz) => h1.
by move: (proj1(BZgcd_div az bz)); rewrite h1; qw.
Qed.
Definition BZ_Bezout a b :=
exists u v, [/\ inc u BZ, inc v BZ & \1z = (a *z u) +z (b *z v)].
Lemma BZ_exists_Bezout1 a b: inc a BZ -> inc b BZ ->
BZ_coprime a b -> BZ_Bezout a b.
Proof.
rewrite /BZ_coprime;red; move => az bz <-; exact (BZgcd_prop2 az bz).
Qed.
Lemma BZ_exists_Bezout2 a b: inc a BZ -> inc b BZ ->
BZ_Bezout a b -> BZ_coprime a b.
Proof.
move => az bz [x [y [xz yz etc]]]; red; symmetry.
apply:(BZ_gcd_unq az bz (sub_BZps_BZp BZps1)).
set_extens t.
move => /funI_P [z zz]; rewrite (BZprod_1l zz) => ->.
move: (BZSp xz zz)(BZSp yz zz) => pa pb.
apply /Zo_P;split => //; exists (x *z z);exists (y *z z);split => //.
rewrite (BZprodA az xz zz) (BZprodA bz yz zz).
rewrite - (BZprod_sumDl zz (BZSp az xz)(BZSp bz yz)) -etc; qw; qprops.
move => /Zo_P [tz _]; apply /funI_P; ex_tac; symmetry;exact (BZprod_1l tz).
Qed.
Lemma BZ_exists_Bezout3 a b: inc a BZ -> inc b BZ ->
(a<> \0z \/ b <> \0z) ->
BZ_Bezout (a %/z (BZgcd a b)) (b %/z (BZgcd a b)).
Proof.
move => az bz h.
move:(BZgcd_prop2 az bz); set g := (BZgcd a b); move => [x [y [xz yz]]].
move: (BZgcd_div az bz) => []; rewrite -/g => p1 p2.
rewrite {1} p1 {1} p2; set qa := (a %/z g); set qb:= (b %/z g).
move: (sub_BZp_BZ (BZpS_gcd az bz)) => gz.
move: (BZS_quo az gz) (BZS_quo bz gz) => pa pb.
rewrite - (BZprodA gz pa xz) - (BZprodA gz pb yz).
rewrite - (BZprod_sumDr gz (BZSp pa xz) (BZSp pb yz)).
rewrite/g - {1} (BZprod_1r gz) => h1.
exists x; exists y;split => //.
apply: (BZprod_reg_l BZS1 _ gz (BZgcd_nz1 az bz h) h1); apply:BZSs; qprops.
Qed.
Lemma BZ_exists_Bezout5 a: inc a BZ -> BZ_coprime a \1z.
Proof.
move: BZS1 => oz az;apply (BZ_exists_Bezout2 az oz).
by exists \0z;exists \1z;split => //; qprops; qw.
Qed.
Definition BZdvdordering := graph_on BZdivides BZps.
Lemma BZdvds_pr6 a b: inc a BZ -> inc b BZ -> a<> \0z ->
(BZdivides a b <-> sub (BZ_ideal1 b)(BZ_ideal1 a)).
Proof.
move => az bz anz ; split.
move => d1 x /funI_P [y yz ->].
move: (BZdvds_pr d1) ->.
rewrite -( BZprodA az (BZS_quo bz az) yz); apply /funI_P.
exists ((b %/z a) *z y) => //; qprops.
move=> h; move: (h _ (proj2 (BZ_in_ideal4 bz))) => /funI_P [z zz ->].
rewrite BZprodC; apply: (BZdvds_pr1 zz az anz).
Qed.
Lemma BZdvds_pr6' a b: BZdivides a b -> sub (BZ_ideal1 b)(BZ_ideal1 a).
Proof.
move => h; move: (h) => [pa pb pc _].
by apply/(BZdvds_pr6 pb pa pc).
Qed.
Lemma BZdvds_monotone a b: inc b BZps -> a %|z b -> a <=z b.
Proof.
move => /BZps_iP [bzp bnz] dvd; move: (dvd) => [_ az _ zz].
case /BZ_i0P: az => ap.
by split => //; qprops; constructor 2; rewrite (BZp_pr2 bzp) (BZms_pr2 ap).
move: (BZdvds_pr dvd) ->; apply: (BZprod_Mpp ap).
apply /BZps_iP;split => //; first by apply : (BZpS_quo bzp ap).
move => h; move: dvd => [_ _ _].
rewrite /BZrem h BZprod_0r BZdiff_0r; qprops.
Qed.
Lemma BZdvdordering_or: order BZdvdordering.
Proof.
have aux: forall t, inc t BZps -> [/\ inc t BZ, inc t BZp & t <> \0z].
move => t /BZps_iP [h unz]; split => //; exact (sub_BZp_BZ h).
apply: order_from_rel1.
move => y x z pa pb; apply: (BZdvds_trans pb pa).
move => u v pa pb d1 d2.
move: (BZdvds_monotone pa d2)(BZdvds_monotone pb d1) => l1 l2; BZo_tac.
move => u h; move: (aux _ h) => [uz _ unz].
exact (proj1 (BZdvd_itself uz unz)).
Qed.
Lemma BZgcd_prop3 a b: inc a BZ -> inc b BZ -> (a<> \0z \/ b <> \0z) ->
let dvd_sup_pr := fun g =>
[/\ g %|z a, g %|z b & forall u, u %|z a -> u %|z b -> u %|z g]
in ( dvd_sup_pr (BZgcd a b)
/\ forall g, dvd_sup_pr g -> (BZgcd a b) = BZabs g).
Proof.
move => az bz abnz prop.
move: (BZgcd_nz1 az bz abnz) => gnz.
move: (BZS_gcd az bz) => gz.
move: (BZgcd_div az bz) => [pa pb].
move: (BZS_quo az gz)(BZS_quo bz gz) => sa sb.
set G := BZgcd a b.
have r1:G %|z a by rewrite pa BZprodC;apply:(BZdvds_pr1 sa gz gnz).
have r2:G %|z b by rewrite pb BZprodC;apply:(BZdvds_pr1 sb gz gnz).
have r3:forall u : Set, u %|z a -> u %|z b -> u %|z G.
move => u ua ub; move: (ua) => [_ uz unz _].
move: (BZS_quo az uz) (BZS_quo bz uz) => paz pbz.
rewrite /G;move: (BZgcd_prop2 az bz) => [x [y [xz yz ->]]].
move: (BZSp paz xz) (BZSp pbz yz) => qaz qbz.
rewrite (BZdvds_pr ua) (BZdvds_pr ub) - (BZprodA uz paz xz).
rewrite - (BZprodA uz pbz yz)- (BZprod_sumDr uz qaz qbz) BZprodC.
apply: (BZdvds_pr1 (BZSs qaz qbz) uz unz).
split; first by split.
move => g [gp1 gp2 gp3].
move: (extensionality (BZdvds_pr6' (gp3 _ r1 r2))(BZdvds_pr6' (r3 _ gp1 gp2))).
move: (gp1)(r1) => [_ gZ _ _] [_ GZ _ _].
move=> et; rewrite (BZ_ideal_unique_gen gZ GZ et).
by rewrite /G (BZabs_pos (BZpS_gcd az bz)).
Qed.
Lemma BZlcm_prop2 a b (l := BZlcm a b):
inc a BZ -> inc b BZ -> a<> \0z -> b <> \0z ->
[/\ a %|z l, b %|z l & forall u, a %|z u -> b %|z u -> l %|z u].
Proof.
move => az bz anz bnz; rewrite /l.
move: (BZlcm_prop1 az bz) => [pa pb pc].
move: (BZS_gcd az bz) => gz.
split; first by rewrite pb BZprodC; apply: (BZdvds_pr1 (BZS_quo bz gz) az anz).
by rewrite pa; apply: (BZdvds_pr1 (BZS_quo az gz) bz bnz).
move => u ua ub.
have h: a <> \0z \/ b <> \0z by left.
move: (BZdvds_pr ua) (BZdvds_pr ub) => r1 r2.
move: (BZ_exists_Bezout3 az bz h) => [x [y [xz yz eq1]]].
move: (f_equal (fun z => z *z u) eq1).
move:(ua) => [uz _ _ _].
move: (BZS_quo az gz) (BZS_quo bz gz) => a'z b'z.
move:(BZS_quo uz bz)(BZS_quo uz az) (BZS_lcm az bz) => ubz uaz lz.
move: (BZSp xz ubz)(BZSp yz uaz) => aaz bbz.
rewrite (BZprod_1l uz) (BZprod_sumDl uz (BZSp a'z xz) (BZSp b'z yz)) => ->.
rewrite (BZprodC _ u) (BZprodA uz a'z xz)(BZprodC _ u) (BZprodA uz b'z yz).
set aux := (u *z (b %/z BZgcd a b)) *z y.
rewrite r2 (BZprodC b) -(BZprodA ubz bz a'z) (BZprodC b) -pa.
rewrite (BZprodC _ x) (BZprodA xz ubz lz); set aux2:= (x *z (u %/z b)).
rewrite /aux r1 (BZprodC a) -(BZprodA uaz az b'z) -pb (BZprodC _ y).
rewrite (BZprodA yz uaz lz) -(BZprod_sumDl lz aaz bbz).
apply: (BZdvds_pr1 (BZSs aaz bbz) lz (BZlcm_nonzero az bz anz bnz)).
Qed.
Lemma BZ_lcm_prop3 a b u: BZ_coprime a b ->
a %|z u -> b %|z u -> (a *z b) %|z u.
Proof.
move => g1 au bu.
move: (au) (bu) => [uz az anz _] [_ bz bnz _].
move: (proj33 (BZlcm_prop2 az bz anz bnz) _ au bu).
by rewrite /BZlcm g1 (BZquo_one (BZSp az bz)).
Qed.
Lemma BZdvdordering_sr: substrate BZdvdordering = BZps.
Proof.
rewrite /BZdvdordering graph_on_sr //.
by move => a /BZps_iP [ap anz]; move: (BZdvd_itself (sub_BZp_BZ ap) anz)=> [].
Qed.
Lemma BZdvdordering_gle x y:
gle BZdvdordering x y <-> [/\ inc x BZps, inc y BZps & x %|z y].
Proof. exact: graph_on_P1. Qed.
Lemma BZpsS_gcd x y: inc x BZps -> inc y BZps -> inc (BZgcd x y) BZps.
Proof.
move => xs ys.
move /BZps_iP: (xs) => [pa xnz]; move: (sub_BZp_BZ pa) => xz.
move /BZps_iP: (ys) => [pb ynz]; move: (sub_BZp_BZ pb) => yz.
have h: (x <> \0z \/ y <> \0z) by left.
apply /BZps_iP; split;[ by apply: BZpS_gcd | exact (BZgcd_nz1 xz yz h)].
Qed.
Lemma BZpsS_lcm x y: inc x BZps -> inc y BZps -> inc (BZlcm x y) BZps.
Proof.
move => xs ys.
move /BZps_iP: (xs) => [pa xnz]; move: (sub_BZp_BZ pa) => xz.
move /BZps_iP: (ys) => [pb ynz]; move: (sub_BZp_BZ pb) => yz.
apply /BZps_iP; split; last by apply: (BZlcm_nonzero xz yz xnz ynz).
rewrite /BZlcm; apply: BZpS_quo; last by apply: BZpS_gcd.
by apply: BZpS_prod.
Qed.
Lemma BZdvd_lattice_aux x y: inc x BZps -> inc y BZps ->
(least_upper_bound BZdvdordering (doubleton x y) (BZlcm x y)
/\ (greatest_lower_bound BZdvdordering (doubleton x y) (BZgcd x y))).
Proof.
move: BZdvdordering_or => or.
move: BZdvdordering_gle => H.
move => xs ys.
move: (BZpsS_gcd xs ys) (BZpsS_lcm xs ys) => gp lp.
move /BZps_iP: (xs) => [pa xnz]; move: (sub_BZp_BZ pa) => xz.
move /BZps_iP: (ys) => [pb ynz]; move: (sub_BZp_BZ pb) => yz.
have h: (x <> \0z \/ y <> \0z) by left.
split.
move: (BZlcm_prop2 xz yz xnz ynz) => [p1 p2 p3].
apply: (lub_set2 or).
by apply /H.
by apply /H.
move => t; move/H => [_ ts ta]/H [_ _ tb]; move: (p3 _ ta tb) => tc.
by apply/H.
move: (BZgcd_prop3 xz yz h) => [[p1 p2 p3] _].
apply: (glb_set2 or);
last (move => t; move/H => [ts _ ta] /H [_ _ tb]; move: (p3 _ ta tb) => tc);
by apply /H.
Qed.
Lemma BZdvd_lattice: lattice BZdvdordering.
Proof.
split; first by apply: BZdvdordering_or.
move => x y; rewrite BZdvdordering_sr => xs ys.
move: (BZdvd_lattice_aux xs ys) => [pa pb].
split; [ by exists (BZlcm x y) | by exists (BZgcd x y) ].
Qed.
Lemma BZdvd_sup x y: inc x BZps -> inc y BZps ->
sup BZdvdordering x y = BZlcm x y.
Proof.
move => xs ys; move: (BZdvd_lattice_aux xs ys) => [pa pb].
symmetry; apply: (supremum_pr2 BZdvdordering_or pa).
Qed.
Lemma BZdvd_inf x y: inc x BZps -> inc y BZps ->
inf BZdvdordering x y = BZgcd x y.
Proof.
move => xs ys; move: (BZdvd_lattice_aux xs ys) => [pa pb].
symmetry; apply: (infimum_pr2 BZdvdordering_or pb).
Qed.
Lemma BZgcd_A a b c: inc a BZ -> inc b BZ -> inc c BZ ->
(BZgcd a (BZgcd b c)) = (BZgcd (BZgcd a b) c).
Proof.
move => az bz cz.
pose id3 u v w := Zo BZ (fun t=> exists x y z,
[/\ inc x BZ, inc y BZ, inc z BZ &
t = u *z x +z (v *z y +z w *z z)]).
have id3a: id3 a b c = id3 c a b.
set_extens t => /Zo_P [tz [x [y [z [xz yz zz etc]]]]]; apply: Zo_i => //.
exists z; exists x; exists y;split => //; rewrite etc (BZsumC (c *z z)).
apply:BZsumA; qprops.
exists y; exists z; exists x; split => //;rewrite etc BZsumC.
symmetry;apply:BZsumA;qprops.
have aux: forall u v w, inc u BZ -> inc v BZ -> inc w BZ ->
BZ_ideal1 (BZgcd u (BZgcd v w)) = id3 u v w.
move => u v w uz vz wz.
move:(BZgcd_prop2 vz wz)=> [uu [vv [uuz vvz etc]]].
rewrite (proj2 (BZgcd_prop1 uz (BZS_gcd vz wz))).
set_extens t; move => /Zo_P [tz h]; apply: (Zo_i tz).
move: h => [c1 [c2 [c1z c2z ->]]]; rewrite etc.
exists c1; exists (uu *z c2); exists (vv *z c2).
rewrite (BZprod_sumDl c2z (BZSp vz uuz) (BZSp wz vvz)).
rewrite - (BZprodA vz uuz c2z) - (BZprodA wz vvz c2z).
move: (BZSp uuz c2z)(BZSp vvz c2z) => sa sb; split => //.
move: h=> [x [y [z [xz yz zz]]]].
move: (BZgcd_div vz wz).
move: (BZS_gcd vz wz) => gz; move: (BZS_quo vz gz)(BZS_quo wz gz).
set q1 := (v %/z BZgcd v w); set q2:=(w %/z BZgcd v w); set g := BZgcd v w.
move => sa sb [-> ->].
move: (BZSp sa yz) (BZSp sb zz) => sc sd; move:(BZSs sc sd) => se.
rewrite - (BZprodA gz sa yz) - (BZprodA gz sb zz).
rewrite - (BZprod_sumDr gz sc sd).
move => ->; exists x; exists ((q1 *z y +z q2 *z z)); split => //.
rewrite (BZgcd_C (BZgcd a b)).
have pa: inc (BZgcd a (BZgcd b c)) BZp by apply: (BZpS_gcd az); qprops.
have pb: inc (BZgcd c (BZgcd a b)) BZp by apply: (BZpS_gcd cz); qprops.
move: (aux _ _ _ az bz cz); rewrite id3a - (aux _ _ _ cz az bz).
move => h; exact: (BZ_ideal_unique_gen1 pa pb h).
Qed.
Lemma BZgcd_prodD a b c: inc a BZ -> inc b BZ -> inc c BZp ->
(BZgcd (c *z a) (c *z b)) = c *z (BZgcd a b).
Proof.
move => az bz cp; move: (sub_BZp_BZ cp) => cz.
case: (equal_or_not c \0z) => cnz.
by rewrite cnz; qw; rewrite (BZgcd_zero BZS0);qw.
case: (equal_or_not b \0z) => bnz.
rewrite bnz; qw; rewrite (BZgcd_zero az) (BZgcd_zero (BZSp cz az)).
by rewrite (BZprod_abs cz az); rewrite (BZabs_pos cp).
move:(BZprod_nz cz bz cnz bnz) => cbnz.
move: (BZgcd_prop3 (BZSp cz az)(BZSp cz bz) (or_intror (c *z a <> \0z) cbnz)).
move => [_ sd].
move: (BZgcd_prop3 az bz (or_intror (a <> \0z) bnz)) => [[sa sb sc] _].
set g := c *z BZgcd a b.
move: (BZpS_gcd az bz) => gzp; move: (sub_BZp_BZ gzp) => gz.
have ->: g = BZabs g.
by rewrite /g (BZprod_abs cz gz) (BZabs_pos cp)(BZabs_pos gzp).
apply: sd;split.
rewrite /g (BZprodC c) (BZprodC c);
by apply /(BZdvds_prod (BZS_gcd az bz) az cz cnz).
rewrite /g (BZprodC c) (BZprodC c);
by apply /(BZdvds_prod (BZS_gcd az bz) bz cz cnz).
move => u u1 u2; move: (BZdvds_pr u1) (BZdvds_pr u2).
move: u1 => [_ uz unz _].
move: (BZS_quo (BZSp cz az) uz) (BZS_quo (BZSp cz bz) uz).
set c1:= ((c *z a) %/z u) ; set c2 := ((c *z b) %/z u) => c1z c2z.
move: (BZgcd_prop2 az bz) => [x [y [xz yz etc]]] e1 e2.
rewrite /g etc (BZprod_sumDr cz (BZSp az xz)(BZSp bz yz)).
rewrite (BZprodA cz az xz)(BZprodA cz bz yz) e1 e2.
rewrite - (BZprodA uz c1z xz) - (BZprodA uz c2z yz).
move: (BZSp c1z xz)(BZSp c2z yz) => qa qb; move: (BZSs qa qb) => qc.
rewrite -(BZprod_sumDr uz qa qb); apply (BZdvds_pr1' qc uz unz).
Qed.
Lemma BZgcd_simp a b c: inc a BZ -> inc b BZ -> inc c BZ ->
BZ_coprime a b -> BZgcd a (b *z c) = BZgcd a c.
Proof.
move => az bz cz cop.
move: (BZ_exists_Bezout1 az bz cop) => [x [y [xz yz etc]]].
move: (f_equal (fun z => z *z c) etc).
rewrite (BZprod_1l cz) (BZprod_sumDl cz (BZSp az xz)(BZSp bz yz)).
rewrite - (BZprodA az xz cz) (BZprodC b) - (BZprodA yz bz cz).
move: (BZSp xz cz); set u := (x *z c) => uz eq1.
case: (equal_or_not a \0z) => anz.
move: (BZSp bz yz) => h.
move:etc; rewrite {1} anz BZprod_0l (BZsum_0l h) => h1; symmetry in h1.
move: (BZprod_1_inversion_l bz yz h1) => [_]; case => ->; qw => //.
by rewrite (BZprod_m1l cz) BZgcd_C - (BZgcd_opp cz az) BZgcd_C.
move: (BZgcd_prop3 az (BZSp bz cz) (or_introl (b *z c <> \0z) anz)) => [_ h].
move: (BZgcd_prop3 az cz (or_introl (c <> \0z) anz)) => [[pa pb pc] _].
rewrite - (BZabs_pos (BZpS_gcd az cz)); apply: h.
split; first by exact.
by apply: (BZdvds_trans2 bz pb).
move=> t ta tb; apply: pc; [ exact | rewrite eq1 ].
have p1: t %|z (a *z u).
exact (BZdvds_trans (BZdvds_pr1' uz az anz) ta).
move: (BZSp az uz) => auz.
case:(equal_or_not (b *z c) \0z) => bcnz; first by rewrite bcnz; qw.
have p2: t %|z (y *z (b *z c)).
rewrite BZprodC.
exact: (BZdvds_trans (BZdvds_pr1' yz (BZSp bz cz) bcnz) tb).
exact (proj1(BZdvd_and_sum p1 p2)).
Qed.
End RationalIntegers.
Export RationalIntegers.