(** * Elements of mathematics: Algebra : Z Copyright INRIA (2010-2012) Apics Marelle Team (Jose Grimm). *) Require Import ssreflect ssrbool eqtype ssrfun. Require Import ZArith. (* $Id: algebra1.v,v 1.13 2012/06/27 16:43:39 grimm Exp$ *) Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. Require Export sset10. Module RationalIntegers. (** ** The set of rational integers *) (** Z is the disjoint union of N* and N; [J x TPb] is positive, [J y TPa] is negative *) Ltac qprops := auto with qprops. Ltac qw := autorewrite with qw. (** We define 0 and the injections [N -> Zp] and [N -> Zm] *) Definition BZ_of_nat x := J x TPb. (** 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 TPa). 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 TPa. Definition BZp:= Bnat *s1 TPb. Definition BZps:= Bnats *s1 TPb. 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. move => t /indexed_P [pa []] /setC1_P [pb pc] pd; apply indexed_P;ee. 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. move => xB xnz; rewrite /BZm_of_nat; Ytac0; apply: indexed_pi; apply /setC1_P;ee. 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. apply /setU1_P; left; apply: indexed_pi; apply /setC1_P;ee. 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 = TPb. 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;ee. by apply /indexed_P;ee. by dneg pe; rewrite pe; qw. move => [] /indexed_P [pa [pb pc]] pd; apply /indexed_P;ee; apply /setC1_P;ee. dneg pe;rewrite /BZ_zero /BZ_of_nat; apply: pair_exten;ee;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; first by move => h; move: (BZms_nz h)=> xnz;ee; apply /setU1_P;left. by move => [] /setU1_P; case. 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. move => h; move: (f_equal P h);rewrite xz /BZ_zero /BZ_of_nat;aw;ee. 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;ee; 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 = TPa \/ Q x = TPb). Proof. apply: candu2_pr2. Qed. Lemma BZp_pr2 x: inc x BZp -> Q x = TPb. Proof. by move /indexed_P => [_ []]. Qed. Lemma BZps_pr2 x: inc x BZps -> Q x = TPb. Proof. by move /indexed_P => [_ []]. Qed. Lemma BZms_pr2 x: inc x BZms -> Q x = TPa. 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;ee. 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. apply/ indexed_P;ee. left; symmetry; apply BZp_hi_pr; apply/ indexed_P;ee. 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 right; right. case (equal_or_not x \0z); [by left | by right ; left; apply /BZps_iP]. case; [ by move => ->;qprops | case => h; qprops ]. Qed. Lemma BZ_i2P x: inc x BZ <-> (inc x BZps \/ inc x BZm). Proof. split. case /BZ_i1P; first by move => ->; right; apply /setU1_P;right. case => xs; [by left | by right; apply /setU1_P;left]. case => xs; qprops. 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 = TPb -> 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 = TPa -> 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 /cardinal_equipotentP; symmetry;apply cardinal_comp_singl_inf. apply: infinite_Bnat. Qed. Lemma infinite_countable_Z: BZ \Eq Bnat. Proof. apply /cardinal_equipotentP. have ->: cardinal BZ = Bnats +c Bnat by []. have ->: Bnats +c Bnat = cardinal Bnat +c cardinal Bnat. apply: csum2_pr4; fprops; eqtrans Bnat; apply: equipotent_Bnats_Bnat. apply:sum2_infinite1; apply /infinite_setP; apply: infinite_Bnat. Qed. (** ** Opposite *) (** The oppositive of a number is obtained by swapping TPa and TPb in the second component, except for zero *) Definition BZopp x:= Yo (Q x = TPa) (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 = TPa -> Q (BZopp x) = TPb) /\ (Q x = TPb -> Q (BZopp x) = TPa)). Proof. move => pa pb. have pnz: (P x <> \0c) by move => h; case pb; apply: BZ_0_if_abs0. rewrite /BZopp /BZ_of_nat /BZm_of_nat; Ytac0;Ytac sx; aw; rewrite ? sx;ee. 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. move => pa pb;apply /setU1_P; left; apply BZopp_positive1; apply /BZps_iP;ee. 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) TPa) => 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;ee. 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 => [_]. move => [pa pb]; apply /indexed_P;ee. 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);ee;qprops; by apply BZopp_K. Qed. Lemma BZopp_p x: BZopp (BZ_of_nat x) = BZm_of_nat x. Proof. by rewrite /BZopp /BZ_of_nat; aw; Ytac0. Qed. Lemma BZopp_m x: BZopp (BZm_of_nat x) = BZ_of_nat x. Proof. rewrite /BZm_of_nat; Ytac bz; first by rewrite BZopp_0 bz. by rewrite /BZopp; aw; Ytac0. Qed. Lemma BZopp_m1: BZopp \1mz = \1z. Proof. by rewrite /BZ_mone BZopp_m. Qed. Lemma BZopp_1: BZopp \1z = \1mz. Proof. by rewrite /BZ_one BZopp_p. Qed. Hint Resolve BZmsS_m1:qprops. (** ** Absolute value *) (** Absolute value is the number with a positive sign; and same numeric value *) Definition BZabs x := BZ_of_nat (P x). Lemma BZabs_pos: forall x, inc x BZp -> BZabs x = x. Proof. move => xz; apply:BZp_hi_pr. Qed. Lemma BZabs_neg x: inc x BZms -> BZabs x = BZopp x. Proof. by move => xz; rewrite /BZabs /BZopp (BZms_pr2 xz); Ytac0. Qed. Lemma BZabs_m1: BZabs \1mz = \1z. Proof. by rewrite (BZabs_neg BZmsS_m1) BZopp_m1. Qed. Lemma BZabs_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) = TPb. Proof. rewrite /BZabs /BZ_of_nat; aw. Qed. Lemma BZabs_abs x: BZabs (BZabs x) = BZabs x. Proof. by rewrite /BZabs BZabs_pr1. Qed. Lemma BZabs_opp x: BZabs (BZopp x) = BZabs x. Proof. by rewrite /BZabs BZopp_pr1. Qed. Lemma BZabs_0 : BZabs \0z = \0z. Proof. by rewrite /BZabs BZ0_pr1. Qed. Hint Rewrite BZabs_0: qw. Lemma BZabs_0p x: inc x BZ -> BZabs x = \0z -> x = \0z. Proof. move => pa pb; move: (f_equal P pb); rewrite BZabs_pr1 BZ0_pr1. apply: (BZ_0_if_abs0 pa). Qed. Hint Resolve BZSa: qprops. (** ** Ordering on Z*) (** We use the ordinal sum of the opposite ordering of Ns and N. This is clearly a total ordering *) Definition BZ_ordering:= order_sum2 (opposite_order (induced_order Bnat_order Bnats)) Bnat_order. Lemma BZ_order_aux1: sub Bnats (substrate Bnat_order). Proof. by rewrite Bnat_order_sr => t /setC1_P []. Qed. Lemma BZ_order_aux: order (opposite_order (induced_order Bnat_order Bnats)) /\ order Bnat_order. Proof. move: Bnat_order_wor => [or _]; move: BZ_order_aux1 => h. ee; 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 _]; move: BZ_order_aux1 => s1. have pc: order (induced_order Bnat_order Bnats) by fprops. by rewrite orsum2_sr //; fprops; aw; rewrite Bnat_order_sr. Qed. Lemma BZor_tor: total_order BZ_ordering. Proof. move:BZ_order_aux1 => h1. move: (worder_total 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 = TPa /\ Q y = TPa /\ (P y) <=c (P x)) \/ (Q x = TPa /\ Q y = TPb) \/ (Q x = TPb /\ Q y = TPb /\ (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 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 = TPa \/ Q z = TPb. move => z /candu2P [_]; case; move => [_ ->]; auto. move => [ra [rb rc]]; red;ee; case: rc. move => [rd [re]] /opposite_gleP => h; left;ee. by move: (iorder_gle1 h) => /Bnat_order_leP [_ [_]]. case. move => [rd [re]] /Bnat_order_leP [_ [_ rf]]; right; right;ee. case (hh _ ra) => //. case (hh _ rb) => //. move => [rd re]; right; left;ee;case (hh _ rb) => qv; intuition. move => [ra [rb rc]];ee. move /candu2P: ra => [_ ra]; move /candu2P: rb => [_ rb]. case: rc. move => [rd [re rf]]; left;ee. 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 /opposite_gleP; apply /iorder_gleP => //. apply /Bnat_order_leP; red;ee. by case /setC1_P: p2 => []. by case /setC1_P: p1. case; first by move => [rd re]; right; right;ee; rewrite re=>h; case TP_ne. move => [rd [re rf]]; right;left;ee. 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 _] ]. apply /Bnat_order_leP; red;ee. 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 False. Proof. by move => pa [pb]; case; apply:BZ_leA. Qed. Lemma BZ_lt_leT a b c: a b <=z c -> a [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 a 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 apply: (BZ_lt_leT Ha Hb) | Ha:?a <=z ?b, Hb: ?b apply: (BZ_le_ltT Ha Hb) | Ha: ?a induction Ha; BZo_tac | Ha: ?a <=z ?b, Hb: ?b 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 (proj1 Ha) | Ha: _ <=z ?a |- inc ?a BZ => exact (proj21 Ha) | Ha: ?a exact (proj11 Ha) | Ha: _ exact (proj121 Ha) | Ha: ?a 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 pa pb; case (equal_or_not a b); first by auto. move => na; right;case (BZ_le_to_ee pa pb) => h1; [left | right]; split => //. auto. Qed. Lemma BZ_le_to_el a b: inc a BZ -> inc b BZ -> a <=z b \/ b ca cb; case (BZ_le_to_ell ca cb). by move=> ->; left; BZo_tac. case; [ move => [pa _] |]; auto. 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; last by move => h; red;ee; fprops; apply:sub_BZp_BZ. move => [_ [_]]; rewrite pc. case; first by move => [ba _]; case TP_ne. case; [by move => [ba _]; case TP_ne |by move => [_ []]]. Qed. Lemma BZ_le_pr2 x y: inc x BZp -> inc y BZms -> y pa pb; move:(BZp_pr2 pa) (BZms_pr2 pb) => pc pd. split; first by red;ee; qprops. 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; last by move => h; red;ee; fprops;apply: sub_BZms_BZ. move => [_ [_]]; rewrite pd. case; first by move => [_ []]. by case; [move => [_ ba] | move => [_ [ba _]]]; case TP_ne. 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 left ;ee; move /(BZ_le_P3 ha hb): h. - by right;left;ee. - by move: (BZ_le_pr4 ha hb) => hc. - by right; right ;ee; move /(BZ_le_P1 ha hb): h. case; first by move => [pa [pb pc]]; apply /BZ_le_P3. case; first 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 (P x) pa pb; split. move => [] /(BZ_le_P1 pa pb) => pc pd;split;ee. 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. move: pc;rewrite BZ0_pr2 qx; case; first by move => [ta]; case TP_ne. by case; [move => [_ ta] | move => [_ [ta _]] ]; case TP_ne. move => xp; red;ee;qprops; rewrite BZ0_pr2 BZ0_pr1; right; right. rewrite (BZp_pr2 xp);ee; move: (BZ_pr1 (sub_BZp_BZ xp)) => t; fprops. Qed. Lemma BZ_positive_P1 x: \0z inc x BZps. Proof. split. move => [] /BZ_positive_P pa pb; apply /BZps_iP;ee; fprops. move /BZps_iP => [pa pb]; split; [by apply /BZ_positive_P | auto]. Qed. Lemma BZ_negative_P x: x inc x BZms. Proof. split. move => pa; case /BZ_i0P: (proj11 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 auto. 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 (czero_least_5 pc). - rewrite xnz ynz BZ0_pr1;move :BZS0 =>h; split=> _; fprops; BZo_tac. Qed. Lemma BZabs_positive b: inc b BZ -> b <> \0z -> \0z 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. red; ee; 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); right; right;ee. case; first by move => [pa pb]; rewrite (qa pa) (qd pb); right; left. move => [pa [pb pc]]; rewrite (qb pa) (qd pb); left;ee. Qed. Lemma BZ_le_opp_iso: order_isomorphism BZopp_fun BZ_ordering (opposite_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. red;rewrite (opposite_order_sr or); rewrite /BZopp_fun; aw;ee. fprops. red; ee; aw => x y xz yz; aw; split. by move /BZ_le_P => h; apply /opposite_gleP; apply /BZ_le_P;apply BZ_le_opp. move /opposite_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 (BZopp y) [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 (BZopp y) pa pb; split; first by apply: BZ_lt_opp. by move=> h; move: (BZ_lt_opp h); rewrite (BZopp_K pa) (BZopp_K pb). Qed. (** ** Addition *) Definition BZsum x y:= let abs_sum := (P x) +c (P y) in let abs_diff1 := (P x) -c (P y) in let abs_diff2 := (P y) -c (P x) in Yo (inc x BZp /\ inc y BZp) (BZ_of_nat abs_sum) (Yo ( ~ inc x BZp /\ ~ inc y BZp) (BZm_of_nat abs_sum) (Yo (inc x BZp /\ ~ inc y BZp) (Yo ( (P y) <=c (P x)) (BZ_of_nat abs_diff1) (BZm_of_nat abs_diff2)) (Yo ( (P x) <=c (P y)) (BZ_of_nat abs_diff2) (BZm_of_nat abs_diff1)))). Notation "x +z y" := (BZsum x y) (at level 50). Lemma BZsumC x y: x +z y = y +z x. Proof. rewrite /BZsum. case (p_or_not_p (inc y BZp /\ inc x BZp)) => h. have h': (inc x BZp /\ inc y BZp) by intuition. by Ytac0; Ytac0; rewrite csumC. have h': not (inc x BZp /\ inc y BZp) by intuition. Ytac0; Ytac0. case (p_or_not_p (~ inc y BZp /\ ~ inc x BZp)) => h2. have h2': (~ inc x BZp /\ ~ inc y BZp) by intuition. by Ytac0; Ytac0; rewrite csumC. have h2': ~ (~ inc x BZp /\ ~ inc y BZp) by intuition. Ytac0; Ytac0. case (p_or_not_p (inc y BZp /\ ~ inc x BZp)) => h3. have h3': ~(inc x BZp /\ ~ inc y BZp) by intuition. by Ytac0; Ytac0. have h3': (inc x BZp /\ ~ inc y BZp). split; first by ex_middle bad; case h3; ee; ex_middle bad2; case h2;ee. move => bad; case h3; ee; move => h4; case h; ee. 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_if_rw //;ee. 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 intuition. by rewrite /BZsum; Ytac0; rewrite (Y_if_rw (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) x +z y = (BZm_of_nat ((P y) -c (P x))). Proof. move => pa pb pc; rewrite BZsum_pm // Y_if_not_rw //. 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_if_rw (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:czero_least_5. 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_if_rw (conj yp2 h1)) /BZopp (BZps_pr2 yp); Ytac0. rewrite /BZm_of_nat (Y_if_not_rw (BZps_pr1nz yp)); aw. by rewrite cdiff_n_n; Ytac h4 => //; Ytac0. case /BZ_i1P; first by move => ->; qw => //; qprops. case; first 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_if_rw 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 pb (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; last by case => bz; auto. move: (sub_BZps_BZ az) => az1; move => ->; rewrite /R;qw => //; qprops. move => xz yz; case /BZ_i1P: (xz). move => ->; rewrite /R;qw => //; qprops. case => xs; first 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;ee;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 _ TPb); 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 pc 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 pa pd pb pc h1 h2); rewrite h5 csumC; move => [_]. - have h3: ~(P x <=c Q x) by move => h3; co_tac. move: (cdiff_nz pa 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 pc pb 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 pc h2) => h5. move: (cdiff_nz pa 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 _ TPa); 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: (czero_least_5 aa). have Hf:forall x, inc x BZ -> inc (f x) NN. move => x xz; move: (BZ_pr1 xz) => pb. rewrite /f; Ytac t; apply: setXp_i; fprops. have Hg:forall x, inc x NN -> inc (g x) BZ. move => x /setX_P [_ [pa pb]]; rewrite /g; Ytac aux. by apply: BZ_of_nat_i; apply:BS_diff. by apply: BZm_of_nat_i; apply:BS_diff. have Hh:forall u v, inc u NN -> inc v NN -> inc (h u v) NN. move => u v /setX_P [_ [pa pb]] /setX_P [_ [pc pd]]; apply: setXp_i; fprops. move => x y z xZ yZ zZ; move: (BZSs xZ yZ) (BZSs yZ zZ). set (yz:= y +z z); set (xy:= x +z y) => xyZ yzZ. have : (g (f yz) = g (h (f y) (f z))) by rewrite Ha // /yz - (H _ _ yZ zZ). move /(Hu _ _ (Hf _ yzZ) (Hh _ _ (Hf _ yZ) (Hf _ zZ))) => eq1. have: (g (f xy) = g (h (f x) (f y))) by rewrite Ha // /xy - (H _ _ xZ yZ). move /(Hu _ _ (Hf _ xyZ) (Hh _ _ (Hf _ xZ) (Hf _ yZ))) => eq2. rewrite (H _ _ xZ yzZ) (H _ _ xyZ zZ). apply /(Hu _ _ (Hh _ _ (Hf _ xZ) (Hf _ yzZ)) (Hh _ _ (Hf _ xyZ) (Hf _ zZ))). move: eq1 eq2;rewrite /h !pr1_pair !pr2_pair. move: (Hf _ xZ) => /setX_P [_ []]. move: (Hf _ yZ) => /setX_P [_ []]. move: (Hf _ zZ) => /setX_P [_ []]. move: (Hf _ xyZ) => /setX_P [_ []]. move: (Hf _ yzZ) => /setX_P [_ []]. set (Px:= P (f x)); set (Qx:=Q (f x)); set (Py:= P (f y)); set (Qy:=Q (f y)). set (Pz:= P (f z)); set (Qz:=Q (f z)); set (Pyz:= P (f yz)). set (Qyz:= Q (f yz)) ; set (Pxy:= P (f xy)); set (Qxy:= Q (f xy)). move => pyzb qyzb pxyb qxyb pzb qzb pyb qyb pxb qxb eq1 eq2. apply: (csum_simplifiable_right qyb); [ fprops | fprops |]. rewrite - csumA - csumA. set a := Pyz +c _. have -> : a = (Pyz +c (Qy +c Qz)) +c Qxy. rewrite /a - (csumA _ _ Qxy); congr (Pyz +c _). by rewrite csumC (csumC Qxy) csumA. set b := _ +c Qy. have -> : b = ((Pxy +c (Qx +c Qy)) +c Qyz) +c Pz. rewrite /b - !csumA; congr (Pxy +c _). by rewrite csumC - !csumA (csumA Qyz Qy Pz) (csumC Qyz Qy) (csumA Qy Qyz Pz). rewrite eq1 eq2 - !csumA; congr (Px +c _); congr (Py +c _). by rewrite csumC (csumC _ Qxy) csumA. Qed. Lemma BZsum_permute_2_in_4 a b c d: inc a BZ -> inc b BZ -> inc c BZ -> inc d BZ -> (a +z b) +z (c +z d) = (a +z c) +z (b +z d). Proof. move => az bz cz dz. rewrite (BZsumA (BZSs az bz) cz dz) (BZsumC a) - (BZsumA bz az cz). by rewrite (BZsumA (BZSs az cz) bz dz) (BZsumC b). Qed. (** ** Multiplication *) Definition BZprod x y := let aux := BZ_of_nat ((P x) *c (P y)) in (Yo (Q x = Q y) aux (BZopp aux)). Notation "x *z y" := (BZprod x y) (at level 40). Definition BZprod_sign_aux x y:= Yo (x = \0z) TPb (Yo (y= \0z) TPb (Yo (Q x = Q y) TPb TPa)). 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_if_not_rw //; 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_if_not_rw 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 => aux; case /BZ_i1P: pb; first by move => ->; qw. case => h1; case aux => h2. - rewrite (BZprod_pp (sub_BZps_BZp h2) (sub_BZps_BZp h1)). by rewrite(BZprod_pm (sub_BZps_BZp h2) (BZopp_positive1 h1)) BZopp_pr1 BZopp_p. - rewrite (BZprod_mp h2 (sub_BZps_BZp h1)). by rewrite (BZprod_mm h2 (BZopp_positive1 h1)) BZopp_pr1 BZopp_m. - rewrite (BZprod_pm (sub_BZps_BZp h2) h1). rewrite (BZprod_pp (sub_BZps_BZp h2) (sub_BZps_BZp (BZopp_negative1 h1))). by rewrite BZopp_pr1 BZopp_m. - rewrite (BZprod_mm h2 h1) (BZprod_mp h2 (sub_BZps_BZp (BZopp_negative1 h1))). 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 = TPa \/ Q t = TPb. move => t /candu2P [_]; case; move => [_]; auto. 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 qc))). 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 qc qb) => dB. Ytac0; Ytac0;rewrite (BZprod_pm pa' (BZm_of_natms_i dB (cdiff_nz qc 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. case; first 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: (ctwo_small (CS_Bnat pa) xnz px1) => le1. move: (cone_small_1 (CS_Bnat pb) ynz) cardinal_lt12 => 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 left. move: (BZprod_reg_l BZS1 (BZSp bz cz) az anz h) => h1; symmetry in h1. by right; move: (BZprod_1_inversion_l bz cz h1) => [_]. Qed. Lemma BZsum_xx n : inc n BZ -> n +z n = n *z \2z. Proof. move => nz; rewrite BZprodC. have aux: inc \2z BZp by apply: BZ_of_natp_i; fprops. have Ha: forall m, inc m BZp -> m +z m = \2z *z m. move => m mp; rewrite (BZsum_pp mp mp) - two_times_n (BZprod_pp aux mp). rewrite /BZ_two /BZ_of_nat; aw. case /BZ_i0P: nz => sx; last by apply: Ha. move: (sub_BZps_BZp (BZopp_negative1 sx)) => pa. move: (sub_BZp_BZ pa) => pb. rewrite - (BZopp_K (sub_BZms_BZ sx)) - (BZsum_opp_distr pb pb) (Ha _ pa). by move: (BZopp_prod_r BZS2 pb). Qed. Lemma BZprod_succ_r n m: inc n BZ -> inc m BZ -> n *z (BZsucc m) = (n *z m) +z n. Proof. by move => pa pb; rewrite /BZsucc (BZprod_sumDr pa pb BZS1) BZprod_1r. Qed. Lemma BZprodt_succ_l n m: inc n BZ -> inc m BZ -> (BZsucc n) *z m = (n *z m) +z m. Proof. by move => pa pb; rewrite BZprodC (BZprod_succ_r pb pa) BZprodC. Qed. (** ** The sign function *) Definition BZsign x:= Yo (P x = \0c) \0z (Yo (Q x = TPb) \1z \1mz). Lemma BZsign_trichotomy a: BZsign a = \1z \/ BZsign a = \1mz \/ BZsign a = \0z. Proof. rewrite /BZsign; Ytac pa; [ by auto | Ytac pb; auto ]. 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); first by move => ->; qw. case => xs; first 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); first by move => ->; qw. case => xs; first 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 pa 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 inc (b -z a) BZps). Proof. move => pa pb; split. move => [] /(BZ_le_diffP pa pb) => pc pd; apply /BZps_iP;ee. 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 \0z 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 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 (c +z a) 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 (a +z c) 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 (proj21 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:Z) := match n with | Z0 => \0z | Zpos p => BZ_of_nat (nat_to_B (nat_of_P p)) | Zneg p => BZm_of_nat (nat_to_B (nat_of_P p)) end. Lemma BZ_of_Z_inc x: inc (BZ_of_Z x) BZ. Proof. case x; first by simpl; qprops. move => p; apply:BZ_of_nat_i; apply: nat_to_B_Bnat. move => p; simpl; apply:BZm_of_nat_i; apply: nat_to_B_Bnat. Qed. Lemma positive_non_zero (p: positive) : inc (nat_to_B (nat_of_P p)) Bnats. Proof. apply /setC1_P; split; first by apply: nat_to_B_Bnat. have <-: nat_to_B 0 = \0c by done. move => h; move: (lt_O_nat_of_P p); rewrite (nat_to_B_injective h). apply: (lt_irrefl 0). Qed. Lemma positive_non_zero1 (p: positive) : inc (BZ_of_nat (nat_to_B (nat_of_P p))) BZps. Proof. by move: (positive_non_zero p) => p1; apply: indexed_pi. Qed. Lemma positive_non_zero2 (p: positive) : inc (BZm_of_nat (nat_to_B (nat_of_P p))) BZms. Proof. by move: (positive_non_zero p) => /setC1_P [pa pb]; apply BZm_of_natms_i. Qed. Lemma BZ_of_Z_injective x y : BZ_of_Z x = BZ_of_Z y -> x = y. Proof. move: positive_non_zero1 positive_non_zero2 => p1 p2. case :x; case:y; simpl. - done. - move => pp pa; symmetry in pa; case (BZps_nz (p1 pp) pa). - move => pp pa; symmetry in pa; case (BZms_nz (p2 pp) pa). - move => pp pa; case (BZps_nz (p1 pp) pa). - move => pa pb eq. by rewrite (nat_of_P_inj _ _ (nat_to_B_injective (BZ_of_nat_inj eq))). - move => pa pb => eq; move: (p1 pb) (p2 pa); rewrite eq => r1 r2. case (BZ_di_neg_spos r2 r1). - move => pp pa; case (BZms_nz (p2 pp) pa). - move => pa pb => eq; move: (p1 pa) (p2 pb); rewrite eq => r1 r2. case (BZ_di_neg_spos r2 r1). - move => pa pb eq. by rewrite (nat_of_P_inj _ _ (nat_to_B_injective (BZm_of_nat_inj eq))). Qed. Lemma BZ_of_Z_surjective x : inc x BZ -> exists y, BZ_of_Z y = x. Proof. case /BZ_i1P; first by move => ->; exists 0%Z; simpl. case. move => pa; rewrite - (BZp_hi_pr (sub_BZps_BZp pa)). move /indexed_P: pa => [_ [pc _]]; move/setC1_P: pc => [pB]. move: (nat_to_B_surjective pB) => [n ->]. case n; [ done| move => m _];exists (Zpos (P_of_succ_nat m)) => /=. by rewrite nat_to_B_succ nat_of_P_o_P_of_succ_nat_eq_succ. move => pa; move: (BZms_hi_pr pa) => [_ <- ]. move /indexed_P: pa => [_ [pc _]]; move/setC1_P: pc => [pB]. move: (nat_to_B_surjective pB) => [n ->]. case n; [ done| move => m _];exists (Zneg (P_of_succ_nat m)) => /=. by rewrite nat_to_B_succ nat_of_P_o_P_of_succ_nat_eq_succ. 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 = \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 (Zopp x) = BZopp (BZ_of_Z x). Proof. case x; first by simpl; qw. - by move => p; simpl; rewrite BZopp_p. - by move => p; simpl; rewrite BZopp_m. Qed. Lemma BZ_of_Z_neg p: BZ_of_Z (Zneg p) = BZopp (BZ_of_Z (Zpos p)). Proof. have -> : (Zneg p = Zopp (Zpos p)) by []. by rewrite BZ_of_Z_opp. Qed. Lemma BZ_of_Z_abs x: BZ_of_Z (Zabs x) = BZabs (BZ_of_Z x). Proof. case x; first by simpl; qw. move => p;simpl; symmetry. apply: BZabs_pos. apply: (sub_BZps_BZp (positive_non_zero1 p)). move => p;simpl; move: (positive_non_zero p); set t := (nat_to_B (nat_of_P p)). move /setC1_P => [ta tb]; rewrite /BZm_of_nat /BZabs; Ytac0; aw. Qed. Lemma BZ_of_Z_sign x: BZ_of_Z (Zsgn x) = BZsign (BZ_of_Z x). Proof. case x => /=; rewrite ?succ_zero. - by rewrite BZsign_0. - by move => p; rewrite (BZsign_pos (positive_non_zero1 p)). - by move => p; rewrite (BZsign_neg (positive_non_zero2 p)). Qed. Lemma BZ_of_Z_prod x y: BZ_of_Z (x * y ) = (BZ_of_Z x) *z (BZ_of_Z y). Proof. move:nat_of_P_mult_morphism => H. move: positive_non_zero1 positive_non_zero2 => H1 H2. case x; first by simpl; qw. - move => p; case y; first by qw. + move => q /=. move:(sub_BZps_BZp (H1 p)) (sub_BZps_BZp (H1 q)) => pa pb. by rewrite H nat_to_B_prod (BZprod_pp pa pb) !BZ_of_nat_pr1. + move => q /=. move:(sub_BZps_BZp (H1 p)) (H2 q) => pa pb. by rewrite H nat_to_B_prod (BZprod_pm pa pb) BZ_of_nat_pr1 BZm_of_nat_pr1. - move => p; case y; first by qw. + move => q /=. move:(sub_BZps_BZp (H1 q)) (H2 p) => pa pb. by rewrite H nat_to_B_prod (BZprod_mp pb pa) BZ_of_nat_pr1 BZm_of_nat_pr1. + move => q /=. by rewrite H nat_to_B_prod (BZprod_mm (H2 p)(H2 q)) ! BZm_of_nat_pr1. Qed. Lemma BZ_of_Z_sum x y: BZ_of_Z (x + y) = (BZ_of_Z x) +z (BZ_of_Z y). Proof. move: positive_non_zero1 => Ha. have Hb: forall p q, BZ_of_Z (Zpos p + Zpos q) = BZ_of_Z (Zpos p) +z BZ_of_Z (Zpos q). move => p q; move: (sub_BZps_BZp (Ha p)) (sub_BZps_BZp (Ha q)) => pa pb. rewrite (BZsum_pp pa pb) ! BZ_of_nat_pr1 /= nat_of_P_plus_morphism. by rewrite nat_to_B_sum. have Hc: forall p, BZ_of_Z (Zpos p) +z BZ_of_Z (Zneg p) = \0z. move =>q. have pa: inc (BZ_of_Z (Zneg q)) BZ by apply:BZ_of_Z_inc. move: (sub_BZps_BZ (Ha q)) => pb. rewrite - (BZopp_K pa) -BZ_of_Z_opp /= -/(_ -z _) (BZdiff_diag) //. have Hd: forall p z, BZ_of_Z (Zpos p + z) = BZ_of_Z (Zpos p) +z (BZ_of_Z z). move => p; case. + simpl; qw => //; apply: BZ_of_nat_i. by move: (positive_non_zero p) => /setC1_P []. + move => q; by apply: Hb. move => q; set rhs := BZ_of_Z (Zpos p) +z BZ_of_Z (Zneg q). set cp := Pcompare p q Eq. have: cp = Eq -> BZ_of_Z 0 = rhs. by move => cpv; rewrite /rhs (Pcompare_Eq_eq _ _ cpv) Hc. have: cp = Lt -> BZ_of_Z (Zneg (q - p)) = rhs. move => h; move: (Pplus_minus _ _ (ZC2 _ _ h)). set n:= (q - p)%positive => np. have pa: inc (BZ_of_Z (Zpos p)) BZ by apply:BZ_of_Z_inc. have pb: inc (BZ_of_Z (Zneg n)) BZ by apply:BZ_of_Z_inc. have pc: inc (BZ_of_Z (Zpos n)) BZ by apply:BZ_of_Z_inc. rewrite /rhs (BZ_of_Z_neg q) - np Zpos_plus_distr Hb. rewrite (BZsum_opp_distr pa pc) (BZsumA pa (BZSo pa) (BZSo pc)). by rewrite - BZ_of_Z_neg Hc - BZ_of_Z_neg (BZsum_0l pb). have: cp = Gt -> BZ_of_Z (Zpos (p - q)) = rhs. move => h; move: (Pplus_minus _ _ h); set n:= (p - q)%positive => np. have pa: inc (BZ_of_Z (Zpos n)) BZ by apply:BZ_of_Z_inc. have pb: inc (BZ_of_Z (Zpos q)) BZ by apply:BZ_of_Z_inc. have pc: inc (BZ_of_Z (Zneg q)) BZ by apply:BZ_of_Z_inc. rewrite /rhs (BZ_of_Z_neg q) - np Zpos_plus_distr Hb - BZ_of_Z_neg BZsumC. by rewrite (BZsumA pc pb pa) (BZsumC (BZ_of_Z (Zneg q))) Hc(BZsum_0l pa). rewrite /Zplus /cp;case (Pcompare p q) => h1 h2 h3; auto. case: x; [by simpl; qw => //; apply: BZ_of_Z_inc | by move => p; apply: Hd |]. move => p. rewrite - (Zopp_involutive (Zneg p + y)) Zopp_plus_distr Zopp_neg BZ_of_Z_opp. move: (BZ_of_Z_inc y) => pa; move: (BZSo pa) => pb. have pc: inc (BZ_of_Z (Zpos p)) BZ by apply:BZ_of_Z_inc. rewrite Hd BZ_of_Z_opp BZsum_opp_distr // - BZ_of_Z_neg BZopp_K //. Qed. Lemma BZ_of_Z_diff x y: BZ_of_Z (x - y ) = (BZ_of_Z x) -z (BZ_of_Z y). Proof. rewrite /Zminus BZ_of_Z_sum BZ_of_Z_opp //. Qed. Lemma BZ_of_Z_succ x: BZ_of_Z (Zsucc x) = BZsucc (BZ_of_Z x). Proof. by rewrite /Zsucc BZ_of_Z_sum BZ_Z_1. Qed. Lemma BZ_of_Z_pred x: BZ_of_Z (Zpred x) = BZpred (BZ_of_Z x). Proof. rewrite /Zpred /BZpred BZ_of_Z_sum BZ_Z_m1 -BZopp_1 //. Qed. Lemma BZ_of_Z_le x y: Zle x y <-> ( (BZ_of_Z x) <=z (BZ_of_Z y)). Proof. apply: iff_sym. apply: (iff_trans (BZ_le_diffP (BZ_of_Z_inc x) (BZ_of_Z_inc y))). rewrite - BZ_of_Z_diff. set z := (y - x )%Z. split. move => pa; apply: Zle_0_minus_le; rewrite -/z. move: pa; case z. - by move => _; apply: Zle_refl. - move => p; rewrite /Zle /= => _; discriminate. - move => p /= pa; case: (BZ_di_neg_pos (positive_non_zero2 p) pa). move => h;move: (Zle_minus_le_0 _ _ h); rewrite -/z; case z. - move => _; apply BZpS0. - move => p _;exact: (sub_BZps_BZp (positive_non_zero1 p)). - by move => p; rewrite /Zle /=. Qed. Lemma BZ_of_Z_lt x y: Zlt x y <-> ( (BZ_of_Z x) h. move: (Zlt_le_weak _ _ h) => /BZ_of_Z_le => h1; split => //. move => sv; move: (BZ_of_Z_injective sv) => eq. by case (Zlt_irrefl x); rewrite {2} eq. move: h => [] /BZ_of_Z_le /Zle_lt_or_eq_iff; case => // -> //. Qed. (** 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: (proj21 eq1) (proj1 eq2)=> cz bz. move /(BZsum_Mleeq (proj1 eq1) cz bz): eq1 => eq3. move/(BZsum_Meqle bz (proj21 eq2) cz): eq2 => eq4. BZo_tac. Qed. Lemma BZsum_Mlelt a b c d: a <=z c -> b (a +z b) eq1 eq2; move: (proj21 eq1) (proj11 eq2)=> cz bz. move /(BZsum_Mleeq (proj1 eq1) cz bz): eq1 => eq3. move/(BZsum_Meqlt bz (proj121 eq2) cz): eq2 => eq4. BZo_tac. Qed. Lemma BZsum_Mltle a b c d: a b <=z d -> (a +z b) eq1 eq2; rewrite (BZsumC a)(BZsumC c); apply:BZsum_Mlelt. Qed. Lemma BZsum_Mltlt a b c d: a b (a +z b) 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 (proj1 pa). Qed. Lemma BZsum_Mlegt0 a c d: a <=z c -> \0z a pa pb; move: (BZsum_Mlelt pa pb); qw => //; exact (proj1 pa). Qed. Lemma BZsum_Mltge0 a c d: a \0z <=z d -> a pa pb; move: (BZsum_Mltle pa pb); qw => //; exact (proj11 pa). Qed. Lemma BZsum_Mltgt0 a c d: a \0z a pa pb; move: (BZsum_Mltlt pa pb); qw => //; exact (proj11 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 (proj21 pa). Qed. Lemma BZsum_Mlelt0 a b c : a <=z c -> b (a +z b) pa pb; move: (BZsum_Mlelt pa pb); qw => //; exact (proj21 pa). Qed. Lemma BZsum_Mltle0 a b c : a b <=z \0z -> (a +z b) pa pb; move: (BZsum_Mltle pa pb); qw => //; exact (proj121 pa). Qed. Lemma BZsum_Mltlt0 a b c : a b (a +z b) pa pb; move: (BZsum_Mltlt pa pb); qw => //; exact (proj121 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 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) 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 nz; rewrite /BZsucc; apply: BZ_sum_Mps => //; apply: BZps1. Qed. Lemma BZ_lt_pred n: inc n BZ -> (BZpred n) 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 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 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 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 TPb) BZp by apply: indexed_pi => //;rewrite /k;fprops. have le2: P (J k TPb) <=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 pm ce1); set k := P m -c P n => knz ce2. rewrite /BZabs /BZm_of_nat; Ytac0; aw. have kz: inc (J k TPb) BZp by apply: indexed_pi => //;rewrite /k;fprops. have le2: P (J k TPb) <=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) <-> (exists 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); split; first by qprops. by rewrite BZsumC; apply:BZsum_diff. have Hc: forall a b c, inc a BZ -> b <=z c -> (Vf b (p a)) <=z (Vf c (p a)). 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 a f) <=z (Vf b f)). 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 (Vf a f) a b [pa pb]; split; first by apply: He. dneg pc; move: (pa) => [xa [xb _]]; rewrite sf in xa xb. exact: (proj12 bf _ _ xa xb pc). have Sa: forall x, inc x BZ -> Vf (BZsucc x) f = (BZsucc (Vf x f)). move => x xz. have pa: inc (Vf x f) BZ by Wtac; fct_tac. move: (BZS_succ pa); rewrite tf => pb; move: (proj22 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 (proj121 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 (BZpred x) f = (BZpred (Vf x f)). 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 \0z f) BZ by rewrite tf; Wtac;[ fct_tac | rewrite - sf; qprops]. ex_tac; rewrite -/(p _); move: (Ha _ fz)(Hb _ fz); set g := p (Vf \0z f). 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 z f = Vf z g)) => //. 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. case /BZ_i1P: az; first by move => ->; qw => /BZps_iP [_]. case /BZ_i1P: bz; first by move => -> _; qw => /BZps_iP [_]. move:BZ_di_neg_spos => H. case => pa; case => pb pc. - split; split => // h; [case (H _ h pb) | case (H _ h pa)]. - case: (H _ _ pc); rewrite BZprodC; exact (BZpmsS_prod pa pb). - case: (H _ _ pc); exact (BZpmsS_prod pb pa). - 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 (a *z c) 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 (b *z c) 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; red;ee. move /indexed_P:h => [_ []]/setC1_P [pc pd] ->;rewrite /BZ_one /BZ_of_nat;aw. right; right;ee; apply cone_small_1; 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 a 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 c (a *z c) 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 c (a *z c) pa pb pc pd. have H: (forall a b, inc a BZp -> a 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 (a *z c) 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. (** ** Division *) Definition BZdivision_prop a b q r := a = (b *z q) +z r /\ r \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. move: (BZ_of_natp_i qb) => pa; move: (sub_BZp_BZ pa) => pb;ee. 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. rewrite /BZrem pa => az; rewrite /BZdiff;qw;ee. 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;ee; 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) TPa) => 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: is_cardinal (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; ee; 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) /\ (inc b BZps -> (BZopp a) %/z b = BZopp (BZsucc (a %/z b))) /\ (BZopp a) %/z b = BZopp ((BZsign b) +z (a %/z b))). Proof. move: a b. suff: forall a b, inc a BZ -> inc b BZp -> b <> \0z -> (P a %%c P b) <> \0c -> ((BZopp a) %%z b = (BZabs b) -z (a %%z b) /\ (BZopp a) %/z b = BZopp (BZsucc (a %/z b))). move => H. move => a b az bz bnz d1; 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. case /BZ_i0P: (bz); last first. move => bp; move: (H _ _ az bp bnz d1) => [r1 r2];ee. rewrite BZsumC BZsign_pos //; apply /BZps_iP;ee. move => bm; rewrite (BZsign_neg bm). move: (BZopp_negative1 bm) => /BZps_iP [qa qb]. have qc: P a %%c P (BZopp b) <> \0c by rewrite BZopp_pr1. move: (H _ _ az qa qb qc) => [e3 e4]. split. rewrite - (BZrem_opp_b (BZSo az) bz) e3 (BZrem_opp_b az bz) BZabs_opp. reflexivity. split; first by move => bp; case (BZ_di_neg_spos bm bp). rewrite (BZsum_opp_distr BZSm1 (BZS_quo az bz)) - (BZquo_opp_b az bz) BZsumC. rewrite -BZopp_1 (BZopp_K BZS1) -/(BZsucc _). have pa: inc (BZopp a %/z b) BZ by apply: BZS_quo; qprops. have pb: inc (BZsucc (a %/z BZopp b)) BZ. apply: BZS_succ; apply: BZS_quo; qprops. by apply :(BZopp_inj pa pb); rewrite -e4 (BZquo_opp_b (BZSo az) bz). move => a b az bz bnz nd; rewrite (BZabs_pos bz). rewrite /BZrem; set q := (a %/z b). suff: BZopp a %/z b = BZopp (BZsucc q). have bza: inc b BZ by qprops. 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 => ->; split => //. 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 b). case (equal_or_not a \0z) => anz. case nd; rewrite anz BZ0_pr1. by move: (cdivision_of_zero (BZ_pr1 (sub_BZp_BZ bz))) => [ [_ [_ ok]] _]. have panz: (P a <> \0c) by move =>h; case anz; exact (BZ_0_if_abs0 az h). rewrite /q /BZquo (BZp_pr2 bz) 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) TPa). 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 qz [pa pb]; ee; red;ee. 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 [pa pb]. move: (proj1 pb) => pz. move:(BZS_diff (proj21 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 rB (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 | case; first 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; ee => 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) 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 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]];ee. - 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' 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 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 //. case ha => bp [s1 s2] [s3 s4]. move/s1: (bp); move/s3: (bp); rewrite (BZsign_pos bp) => s5 s6. move: (aux2 _ _ qz q'z s5) (aux2 _ _ q'z qz s6) => l1 l2; BZo_tac. move/s2: (bp); move/s4: (bp); rewrite (BZsign_neg bp) => 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]. red;ee; qprops. 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);ee; 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]]; red;ee; 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;ee; apply /(BZnon_zero_opp bz). by move => h;ee; 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;ee; 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];ee; red;ee; 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. exact: (BZdvds_trans (BZdvds_pr1 cz (proj1 dv1) 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 \0z. by apply: BZprod_nz => //;move /BZps_iP: czp => [_]. have h: (BZdivision_prop (a *z c) (b *z c) q (r *z c)) by red;ee. move: (BZdvd_unique1 (BZSp az cz) (BZSp bz cz) qz (BZSp rz cz) bcnz h). by move => [-> ->]. 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);ee. 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: (proj1 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, exists 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;ee. exists \1z; exists \0z;qw;ee; qprops. exists \0z; exists \1z;qw;ee; 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 []. split. 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 | split; [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 | split; [qprops | ]]. rewrite (BZprodA az uz yz) (BZprodA bz vz yz). by rewrite - (BZprod_sumDl yz (BZSp az uz) (BZSp bz vz)) -pa. Qed. (** ** Ideals *) 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 /fun_imageP => [x [xz <-]]; apply /Zo_P; split; first by qprops. exists x; exists \0z;ee; [ qprops | qw; qprops]. move=> /Zo_P [xz [u [v [uz [vz pa]]]]]; apply /fun_imageP. by exists (u +z v);split; [ 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: (proj1 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 (proj21 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: (proj22 ix _ _ bx (BZS_quo (proj1 ix _ ax) (proj1 ix _ bx))). Qed. Lemma BZ_ideal_0P a: inc a (BZ_ideal1 \0z) <-> (a = \0z). Proof. split. by move => /fun_imageP [z]; qw; move => [_]. move => az; apply /fun_imageP; exists \0z; split; qw;qprops. Qed. Lemma BZ_N_worder X: sub X BZp -> nonempty X -> exists 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 /fun_imageP [z [zz <-]]; apply: (BZ_pr1 (sub_BZp_BZ (pa _ zz))). have ney: (nonempty Y) by exists (P t); apply /fun_imageP; ex_tac. move: (Bnat_order_wor) => [or wor]. have yb1: sub Y (substrate Bnat_order) by rewrite Bnat_order_sr. move: (wor _ yb1 ney) => [y []]; aw => yy aux. move /fun_imageP: (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 /fun_imageP; ex_tac. by move: (iorder_gle1 (aux _ pby)) => /Bnat_order_leP [_ [_]]. Qed. Theorem BZ_principal x: BZ_ideal x -> nonempty x -> exists a, (inc a BZp /\ BZ_ideal1 a = x). Proof. move => ix nex. case (p_or_not_p (exists a, inc a x /\ a <> \0z)); last first. move => h; exists \0z;split; first by apply: BZpS0. set_extens t. move:nex => [q qx]; move: (proj22 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 (proj1 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/fun_imageP => [u [uz <-]]; apply: (proj22 ix _ _ bx uz). move => tx. move: (BZ_idealS_rem ix tx bx) => rx. move: (BZdvd_correct (proj1 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 /fun_imageP; exists (t %/z b);ee. 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. (* deplacer *) Lemma BZabs_1: BZabs \1z = \1z. Proof. exact (BZabs_pos(sub_BZps_BZp BZps1)). 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 => /fun_imageP [z [zz]] => eq1. move: pb; rewrite sv => /fun_imageP [u [uz]]; rewrite -eq1. rewrite - (BZprodA az zz uz) => aux; symmetry in aux. case (BZprod_1_inversion_more az zz uz aux); first by move => ->; qw. move => h; move: (BZprod_abs az zz); rewrite eq1. move: (BZSa az) => aaz. by case h => ->; 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. (** ** Gcd *) 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: (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:(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) => <-;ee. 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 => [] /fun_imageP [q [qa qb]] /fun_imageP [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, exists 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;ee;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 => //. exists (u -z v *z q); exists v. move:(BZSp vz qz) => vqz; move: (BZS_diff uz vqz)=> ha;ee. 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; ee; 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;ee. 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 => ->;ee; 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, exists 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 => /fun_imageP [z [zz]]; rewrite (BZprod_1l zz) => <-. move: (BZSp xz zz)(BZSp yz zz) => pa pb. apply /Zo_P;ee; exists (x *z z);exists (y *z z);ee. 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 /fun_imageP; ex_tac; 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;ee. 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;ee; 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 /fun_imageP [y [yz]] <-. move: (BZdvds_pr d1) ->. rewrite -( BZprodA az (BZS_quo bz az) yz); apply /fun_imageP. exists ((b %/z a) *z y);ee; qprops. move=> h; move: (h _ (proj2 (BZ_in_ideal4 bz))) => /fun_imageP [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: (proj21 dvd) => az. case /BZ_i0P: az => ap. red;ee; qprops; right; left; rewrite (BZp_pr2 bzp) (BZms_pr2 ap);ee. move: (BZdvds_pr dvd) ->; apply: (BZprod_Mpp ap). apply /BZps_iP;ee; 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]; ee; 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 red;ee. move => g [gp1 [gp2 gp3]]. move: (extensionality (BZdvds_pr6' (gp3 _ r1 r2)) (BZdvds_pr6' (r3 _ gp1 gp2))). move=> et; rewrite (BZ_ideal_unique_gen (proj21 gp1) (proj21 r1) 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). split; first 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: (proj1 ua) (BZS_quo az gz) (BZS_quo bz gz) => uz 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: (proj22 (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 BZdvd_lattice: lattice BZdvdordering. Proof. move: BZdvdordering_or => or. split; first by apply: BZdvdordering_or. rewrite BZdvdordering_sr. move: BZdvdordering_gle => H. move => x y 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. have gp: inc (BZgcd x y) BZps. apply /BZps_iP; split;[ by apply: BZpS_gcd | exact (BZgcd_nz1 xz yz h)]. have lp:inc (BZlcm x y) BZps. 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. split. move: (BZlcm_prop2 xz yz xnz ynz) => [p1 [p2 p3]]. exists (BZlcm x y); apply: (lub_set2 or). - apply /H; ee. - apply /H; ee. - 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]] _]. exists (BZgcd x y); apply: (glb_set2 or). - apply /H;ee. - apply /H;ee. - move => t; move/H => [ts [_ ta]]/H [_ [_ tb]]; move: (p3 _ ta tb) => tc. by apply/H. Qed. End RationalIntegers. Export RationalIntegers.