(** * Algebra : Rational numbers Copyright INRIA (2010) Apics Team (Jose Grimm). *) Require Export algebra1. Set Implicit Arguments. (* \$Id: algebra2.v,v 1.12 2010/08/02 07:30:56 grimm Exp \$ *) Module RationalNumbers. (** ** The set of rational numbers *) Definition BQ_base := product BZ BZps. Definition BQ_related a b := inc a BQ_base & inc b BQ_base & BZmult (P a) (Q b) = BZmult (P b) (Q a). Lemma BQ_base_pr: forall x, inc x BQ_base -> (is_pair x & inc (P x) BZ & inc (Q x) BZps). Proof. ir. ufi BQ_base H. awi H. am. Qed. Lemma BQ_related_refl : forall a, inc a BQ_base -> BQ_related a a. Proof. ir. uf BQ_related. au. Qed. Lemma BQ_related_symm : forall a b, BQ_related a b -> BQ_related b a. Proof. uf BQ_related. ir. eee. Qed. Lemma BQ_related_aux : forall a b c x y, x = BZmult a b -> y = BZmult a c -> inc a BZ -> inc b BZ -> inc c BZ -> BZmult x c = BZmult b y. Proof. ir. rw H. rw H0. rw (BZ_mult_comm a b). rww BZ_mult_assoc. Qed. Lemma BQ_related_trans : forall a b c, BQ_related a b -> BQ_related b c -> BQ_related a c. Proof. uf BQ_related. ir. eee. cp (f_equal (BZmult (Q a)) H2). cp (BQ_base_pr H). cp (BQ_base_pr H0). cp (BQ_base_pr H1). ee. cp (sub_BZps_BZ H14). cp (sub_BZps_BZ H12). cp (sub_BZps_BZ H10). rwii BZ_mult_assoc H5. rwi (BZ_mult_comm (Q a) (P b)) H5. wri H4 H5. rwi (BZ_mult_assoc H15 H9 H16) H5. rwi BZ_mult_comm H5. rwii BZ_mult_assoc H5. rw BZ_mult_comm. rw (BZ_mult_comm (P c) (Q a)). apply BZmult_reg_r with (Q b). am. app BZ_stable_mult. app BZ_stable_mult. rwi inc_BZps H12. eee. am. Qed. Lemma BQ_related_simplify: forall a b c d, inc a BZ -> inc b BZ -> inc c BZ -> inc d BZ -> BZ_coprime a b -> BZmult a d = BZmult b c -> exists e, inc e BZ & d = BZmult b e & c = BZmult a e. Proof. ir. nin (BZ_exists_Bezout1 H H0 H3). nin H5. ee. cp (BZ_stable_mult H H5). cp (BZ_stable_mult H0 H6). cp (f_equal (BZmult d) H7). qwi H10. rwii BZmult_plus_distr_r H10. rwii BZ_mult_assoc H10. rwi (BZ_mult_comm d a) H10. rwi H4 H10. wrii BZ_mult_assoc H10. rwi (BZ_mult_comm d (BZmult b x0)) H10. wrii BZ_mult_assoc H10. wrii BZmult_plus_distr_r H10. cp (f_equal (BZmult c) H7). qwi H11. rwii BZmult_plus_distr_r H11. rwi (BZ_mult_comm a x) H11. rwii BZ_mult_assoc H11. rwi (BZ_mult_comm (BZmult c x) a) H11. rwi (BZ_mult_assoc H1 H0 H6) H11. rwi (BZ_mult_comm c b) H11. wri H4 H11. wri (BZ_mult_assoc H H2 H6) H11. rwi (BZ_mult_comm d x0) H11. wrii BZmult_plus_distr_r H11. exists (BZplus (BZmult c x) (BZmult x0 d)). eee; qprops. app BZ_stable_plus. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. am. app BZ_stable_mult. app BZ_stable_mult. am. Qed. Lemma BQ_related_simplify2: forall a b c d, inc a BZ -> inc b BZ -> inc c BZ -> inc d BZ -> BZ_coprime a b -> BZ_coprime c d -> BZmult a d = BZmult b c -> d <> BZ_zero -> ((a = c & b = d) \/ (a = BZopp c & b = BZopp d)). Proof. ir. nin (BQ_related_simplify H H0 H1 H2 H3 H5). ee. rwi BZ_mult_comm H5. rwi (BZ_mult_comm b c) H5. symmetry in H5. nin (BQ_related_simplify H1 H2 H H0 H4 H5). ee. rwi H11 H8. wri BZ_mult_assoc H8. nin (BZmult_1_inversion_more H2 H10 H7). contradiction. nin H13. rwi H13 H11. qwi H11. rwi H13 H12. qwi H12. au. am. am. rwi H13 H11. rwi BZ_mult_m1_r H11. rwi H13 H12. rwi BZ_mult_m1_r H12. au. am. am. am. am. am. am. Qed. Lemma BQ_related_simplify3: forall a b c d, inc a BZ -> inc b BZps -> inc c BZ -> inc d BZps -> BZ_coprime a b -> BZ_coprime c d -> BZmult a d = BZmult b c -> (a = c & b = d). Proof. ir. cp (sub_BZps_BZ H0). cp (sub_BZps_BZ H2). cp H2. rwi inc_BZps H2. nin H2. nin (BQ_related_simplify2 H H6 H1 H7 H3 H4 H5 H9). am. nin H10. cp (BZopp_positive1 H8). wri H11 H12. elim (BZ_disjoint_neg_spos H12 H0). Qed. Definition BQ := Zo BQ_base (fun z=> BZ_coprime (P z) (Q z)). Definition BQ_rep x := J (BZquo (P x) (BZ_gcd (P x) (Q x))) (BZquo (Q x) (BZ_gcd (P x) (Q x))). Lemma sub_BQbase : sub BQ BQ_base. Proof. ir. uf BQ. app Z_sub. Qed. Lemma BQ_is_graph: forall x, inc x BQ -> x = J (P x) (Q x). Proof. ir. aw. nin (BQ_base_pr (sub_BQbase H)). am. Qed. Lemma BQ_normal_representative : forall x, inc x BQ_base -> (BQ_related x (BQ_rep x) & inc (BQ_rep x) BQ). Proof. ir. cp (BQ_base_pr H). nin H0. nin H1. rwi inc_BZps H2. nin H2. assert (inc (Q x) BZ). qprops. assert (P x <> BZ_zero \/ Q x <> BZ_zero). au. cp (BZ_exists_Bezout3 H1 H4 H5). uf BQ_rep. cp (BZ_gcd_diva H1 H4). cp (BZ_gcd_divb H1 H4). set (g := BZ_gcd (P x) (Q x)) in *. set (w := J (BZquo (P x) g) (BZquo (Q x) g)). assert (inc g BZps). rw inc_BZps. uf g. split. qprops. app BZ_gcd_nonzero1. assert (inc w BQ_base). uf BQ_base. uf w. aw. ee. fprops. qprops. uf g. rw BZ_gcd_comm. rw inc_BZps. split. app BZ_positive_quo_gcd. app BZ_non_zero_quo_gcd. am. am. split. red. eee. uf w. aw. app (BQ_related_aux H7 H8). uf g. qprops. qprops. qprops. uf BQ. Ztac. uf w. aw. app BZ_exists_Bezout2. qprops. qprops. Qed. Lemma BQ_normal_representative_unique : forall x y, inc x BQ -> inc y BQ -> BQ_related x y -> x = y. Proof. ir. ufi BQ H. Ztac. ufi BQ H0. Ztac. nin H1. nin H6. ufi BQ_base H1. awi H1. ufi BQ_base H6. awi H6. ee. rwi (BZ_mult_comm (P y) (Q x)) H7. cp (BQ_related_simplify3 H10 H11 H8 H9 H3 H5 H7). nin H12. app pair_extensionality. Qed. Lemma BQ_rep_involutive: forall x, inc x BQ -> BQ_rep x = x. Proof. ir. assert (inc x BQ_base). ufi BQ H. Ztac. am. cp (BQ_normal_representative H0). ee. app BQ_normal_representative_unique. app BQ_related_symm. Qed. Lemma BQ_normal_representative_unique1 : forall x y, BQ_related x y -> BQ_rep x = BQ_rep y. Proof. ir. assert (inc x BQ_base). nin H. am. nin (BQ_normal_representative H0). assert (inc y BQ_base). nin H. nin H3. am. nin (BQ_normal_representative H3). app BQ_normal_representative_unique. cp (BQ_related_symm H1). cp (BQ_related_trans H6 H). ap (BQ_related_trans H7 H4). Qed. Definition BQp := intersection2 BQ (product BZp BZps). Definition BQm := intersection2 BQ (product BZm BZps). Definition BQps := intersection2 BQ (product BZps BZps). Definition BQms := intersection2 BQ (product BZms BZps). Lemma sub_BQp_BQ : sub BQp BQ. Proof. uf BQp. app intersection2sub_first. Qed. Lemma sub_BQps_BQp : sub BQps BQp. Proof. uf BQps; uf BQp. red; ir. nin (intersection2_both H). awi H1. app intersection2_inc. aw. eee. qprops. Qed. Lemma sub_BQps_BQ : sub BQps BQ. Proof. ap (sub_trans sub_BQps_BQp sub_BQp_BQ). Qed. Lemma sub_BQms_BQm : sub BQms BQm. Proof. uf BQms; uf BQm. red; ir. nin (intersection2_both H). awi H1. app intersection2_inc. aw. eee. qprops. Qed. Lemma sub_BQm_BQ : sub BQm BQ. Proof. uf BQm. app intersection2sub_first. Qed. Lemma sub_BQms_BQ : sub BQms BQ. Proof. ap (sub_trans sub_BQms_BQm sub_BQm_BQ). Qed. Hint Resolve sub_BQm_BQ sub_BQms_BQ sub_BQp_BQ sub_BQps_BQ : qprops. Hint Resolve sub_BQms_BQm sub_BQps_BQp : qprops. Lemma inc_BQp_pr : forall x, inc x BQp = (inc x BQ & inc (P x) BZp). Proof. ir. app iff_eq. ir. split. qprops. ufi BQp H. awi H. cp (intersection2_second H). awi H0. ee; am. ir. nin H. uf BQp. app intersection2_inc. nin (BQ_base_pr (sub_BQbase H)). ee. aw. eee. Qed. Lemma inc_BQps_pr : forall x, inc x BQps = (inc x BQ & inc (P x) BZps). Proof. ir. app iff_eq. ir. split. qprops. ufi BQps H. awi H. cp (intersection2_second H). awi H0. ee; am. ir. nin H. uf BQps. app intersection2_inc. nin (BQ_base_pr (sub_BQbase H)). ee. aw. eee. Qed. Lemma inc_BQm_pr : forall x, inc x BQm = (inc x BQ & inc (P x) BZm). Proof. ir. app iff_eq. ir. split. qprops. ufi BQm H. awi H. cp (intersection2_second H). awi H0. ee; am. ir. nin H. uf BQm. app intersection2_inc. nin (BQ_base_pr (sub_BQbase H)). ee. aw. eee. Qed. Lemma inc_BQms_pr : forall x, inc x BQms = (inc x BQ & inc (P x) BZms). Proof. ir. app iff_eq. ir. split. qprops. ufi BQms H. awi H. cp (intersection2_second H). awi H0. ee; am. ir. nin H. uf BQms. app intersection2_inc. nin (BQ_base_pr (sub_BQbase H)). ee. aw. eee. Qed. Lemma BQps_stable_rep: forall x, inc x BQ_base -> inc (P x) BZps -> inc (BQ_rep x) BQps. Proof. ir. rw inc_BQps_pr. split. qprops. nin (BQ_normal_representative H). am. uf BQ_rep. aw. rw inc_BZps. ufi BQ_base H. awi H. ee. app BZp_stable_quo. qprops. qprops. app BZ_non_zero_quo_gcd. qprops. rwi inc_BZps H0. ee; am. Qed. Definition BQ_of_Z x := J x BZ_one. Definition BQi_of_Z x := J BZ_one x. Lemma BQ_P : forall x, inc x BQ -> inc (P x) BZ. Proof. ir. nin (BQ_base_pr (sub_BQbase H)). ee. am. Qed. Lemma BQ_Qps : forall x, inc x BQ -> inc (Q x) BZps. Proof. ir. nin (BQ_base_pr (sub_BQbase H)). ee. am. Qed. Lemma BQ_Q : forall x, inc x BQ -> inc (Q x) BZ. Proof. ir. cp (BQ_Qps H). qprops. Qed. Hint Resolve BQ_P BQ_P BQ_Qps : qprops. Lemma BQ_extens: forall x y, inc x BQ -> inc y BQ -> P x = P y -> Q x = Q y -> x = y. Proof. ir. rw (BQ_is_graph H). rw (BQ_is_graph H0). ue. ue. Qed. Lemma inc_BQ_of_Z: forall x, inc x BZ -> inc (BQ_of_Z x) BQ. Proof. ir. uf BQ_of_Z. uf BQ. Ztac. uf BQ_base. aw. eee. app inc1_BZps. aw. app BZ_exists_Bezout5. Qed. Lemma inc_BQ_of_Zp: forall x, inc x BZp -> inc (BQ_of_Z x) BQp. Proof. ir. rw inc_BQp_pr. split. app inc_BQ_of_Z. qprops. uf BQ_of_Z. aw. Qed. Lemma inc_BQi_of_Z: forall x, inc x BZps -> inc (BQi_of_Z x) BQ. Proof. ir. uf BQi_of_Z. uf BQ. Ztac. uf BQ_base. aw. eee. qprops. qw. aw. red. rw BZ_gcd_comm. app BZ_exists_Bezout5. qprops. qprops. qprops. Qed. Hint Resolve inc_BQ_of_Z inc_BQi_of_Z: qprops. Lemma BQ_of_Z_inj: forall x y, inc x BZ -> inc y BZ -> BQ_of_Z x = BQ_of_Z y -> x = y. Proof. uf BQ_of_Z. ir. inter2tac. Qed. Definition BQ_zero := BQ_of_Z BZ_zero. Definition BQ_one := BQ_of_Z BZ_one. Definition BQ_two := BQ_of_Z BZ_two. Definition BQ_mone := BQ_of_Z BZ_mone. Definition BQ_half := BQi_of_Z BZ_two. Lemma inc0_BQ : inc BQ_zero BQ. Proof. uf BQ_zero. qprops. Qed. Lemma inc0_BQp: inc BQ_zero BQp. Proof. uf BQ_zero. app inc_BQ_of_Zp. app inc0_BZp. Qed. Lemma inc1_BQp: inc BQ_one BQp. Proof. uf BQ_one. app inc_BQ_of_Zp. uf BZ_one. app inc_BZ_of_natp. fprops. Qed. Lemma inc1_BQ : inc BQ_one BQ. Proof. uf BQ_one. qprops. Qed. Lemma inc2_BQ : inc BQ_two BQ. Proof. uf BQ_two. assert (inc BZ_two BZ). app inc2_BZ. qprops. Qed. Lemma incm1_BQ : inc BQ_mone BQ. Proof. uf BQ_mone. qprops. Qed. Lemma inci2_BQ : inc BQ_half BQ. Proof. uf BQ_half. assert (inc BZ_two BZps). uf BZps. uf BZ_two. uf BZ_of_nat. aw. eee. uf Bnats. Ztac. fprops. app card_two_not_zero. app inc_BQi_of_Z. Qed. Hint Resolve inc0_BQ inc1_BQ inc2_BQ incm1_BQ: qprops. Lemma BQ_zero_P: P BQ_zero = BZ_zero. Proof. uf BQ_zero. uf BQ_of_Z. aw. Qed. Lemma BQ_zero_Q: Q BQ_zero = BZ_one. Proof. uf BQ_zero. uf BQ_of_Z. aw. Qed. Hint Rewrite BQ_zero_P BQ_zero_Q: qw. Lemma BQ_zero_if_num0: forall x, inc x BQ -> P x = BZ_zero -> x = BQ_zero. Proof. ir. set (inc0_BQ). cp (sub_BQbase H). cp (BQ_base_pr H1). ee. app BQ_normal_representative_unique. red. ee. am. app sub_BQbase. qw. qprops. Qed. Lemma BQ_zero_if_num0_bis: forall x, inc x BZps -> BQ_rep (J BZ_zero x) = BQ_zero. Proof. ir. rwii inc_BZps H. nin H. cp (sub_BZp_BZ H). uf BQ_rep. aw. rww BZ_gcd_comm. rw BZ_gcd_zero. rww BZ_abs_pos. rww BZquo_itself. nin (BZ_division_zero H1). rww H2. am. qprops. Qed. Lemma BQs_stable_rep: forall x, inc x BQ_base -> P x <> BZ_zero -> BQ_rep x <> BQ_zero. Proof. ir. uf BQ_rep. red. ir. cp (f_equal P H1). awi H2. qwi H2. cp (BQ_base_pr H). ee. cp (BZ_non_zero_quo_gcd H4 (sub_BZps_BZ H5) H0). contradiction. Qed. Lemma BQ_disjoint_neg_0 : forall x, inc x BQms -> x = BQ_zero -> False. Proof. ir. ufi BQms H. cp (intersection2_second H). awi H1. ee. rwi H0 H2. qwi H2. elim (BZ_disjoint_neg_0 H2). tv. Qed. Lemma BQ_disjoint_pos_0 : forall x, inc x BQps -> x = BQ_zero -> False. Proof. ir. ufi BQps H. cp (intersection2_second H). awi H1. ee. rwi H0 H2. qwi H2. elim (BZ_disjoint_pos_0 H2). tv. Qed. Lemma BQ_disjoint_neg_pos : forall x, inc x BQms -> inc x BQp -> False. Proof. ir. ufi BQms H. ufi BQp H0. cp (intersection2_second H). awi H1. ee. cp (intersection2_second H0). awi H4. ee. elim (BZ_disjoint_neg_pos H2 H5). Qed. Lemma BQ_disjoint_pos_neg : forall x, inc x BQps -> inc x BQm -> False. Proof. ir. ufi BQps H. ufi BQm H0. cp (intersection2_second H). awi H1. ee. cp (intersection2_second H0). awi H4. ee. elim (BZ_disjoint_pos_neg H2 H5). Qed. Lemma BQ_disjoint_neg_spos : forall x, inc x BQms -> inc x BQps -> False. Proof. ir. cp (sub_BQms_BQm H). ap (BQ_disjoint_pos_neg H0 H1). Qed. Lemma inc_BQ1 : forall x, inc x BQ = (x = BQ_zero \/ inc x BQps \/ inc x BQms). Proof. ir. app iff_eq. ir. rw inc_BQps_pr. rw inc_BQms_pr. cp H. ufi BQ H. Ztac. ufi BQ_base H1. awi H1. ee. rwi inc_BZ1 H3. nin H3. left. app BQ_zero_if_num0. nin H3. au. au. ir. nin H. rw H. qprops. nin H; qprops. Qed. Lemma inc_BQ: forall x, inc x BQ = (inc x BQms \/ inc x BQp). Proof. ir. app iff_eq. ir. rw inc_BQms_pr. rw inc_BQp_pr. cp H. ufi BQ H. Ztac. ufi BQ_base H1. awi H1. ee. rwi inc_BZ H3. nin H3. au. au. ir. nin H; qprops. Qed. Lemma inc_BQps_pr1 : forall x, inc x BQps = (inc x BQp & x <> BQ_zero). Proof. ir. ap iff_eq. ir. split. qprops. red. ir. elim (BQ_disjoint_pos_0 H H0). ir. nin H. assert (inc x BQ). qprops. rwi inc_BQ1 H1. nin H1. contradiction. nin H1. am. elim (BQ_disjoint_neg_pos H1 H). Qed. Lemma inc_BQms_pr1 : forall x, inc x BQms = (inc x BQm & x <> BQ_zero). Proof. ir. ap iff_eq. ir. split. qprops. red. ir. elim (BQ_disjoint_neg_0 H H0). ir. nin H. assert (inc x BQ). qprops. rwi inc_BQ1 H1. nin H1. contradiction. nin H1. elim (BQ_disjoint_pos_neg H1 H). am. Qed. Lemma infinite_countable_Q: cardinal BQ = cardinal Bnat. Proof. ir. set (N:= cardinal Bnat). assert (equipotent Bnat N). uf N. fprops. assert (is_cardinal N). uf N. fprops. cp infinite_Bnat. fold N in H1. assert (card_mult N N = N). app product2_infinite. fprops. red. ir. rwi H2 H1. nin H1. elim H3. fprops. assert (equipotent BZ N). eqtrans Bnat. cp infinite_countable_Z. awii H3. am. assert (cardinal BQ_base = N). assert (equipotent BZps N). eqtrans Bnat. uf BZps. eqtrans Bnats. eqsym. app equipotent_a_times_singl. app equipotent_Bnats_Bnat. am. cp (equipotent_product H3 H4). assert (cardinal (product BZ BZps) = cardinal (product N N)). aw. uf BQ_base. rw H6. wrr card_mult_pr1. cp (sub_smaller sub_BQbase). rwi H4 H5. set (f:= BL BQ_of_Z BZ BQ). assert (injective f). uf f. app bl_injective. red. ir. qprops. ir. app BQ_of_Z_inj. cp (cardinal_le9 H6). ufi f H7. awi H7. rwi infinite_countable_Z H7. fold N in H7. co_tac. Qed. Definition BQopp x := J (BZopp (P x)) (Q x). Definition BQabs x := J (BZabs (P x)) (Q x). Lemma BQ_opp_P: forall x, P (BQopp x) = BZopp (P x). Proof. ir. uf BQopp. aw. Qed . Lemma BQ_opp_Q: forall x, Q (BQopp x) = Q x. Proof. ir. uf BQopp. aw. Qed. Lemma BQ_abs_P: forall x, P (BQabs x) = BZabs (P x). Proof. ir. uf BQabs. aw. Qed. Lemma BQ_abs_Q: forall x, Q (BQabs x) = Q x. Proof. ir. uf BQabs. aw. Qed. Lemma BQopp_involutive: forall x, inc x BQ -> BQopp (BQopp x) = x. Proof. ir. cp (BQ_base_pr (sub_BQbase H)). ee. uf BQopp. aw. rw BZopp_involutive. aw. am. Qed. Hint Rewrite BQ_opp_P BQ_opp_Q BQ_abs_P BQ_abs_Q: qw. Lemma BQ_stable_opp: forall a, inc a BQ -> inc (BQopp a) BQ. Proof. ir. ufi BQ H. Ztac. cp (BQ_base_pr H0). ee. uf BQopp. uf BQ. clear H. Ztac. uf BQ_base. aw. eee; qprops. aw. red in H1. rwi BZ_gcd_opp H1. am. am. qprops. Qed. Lemma BQ_opp_related: forall x, inc x BQ_base -> BQopp (BQ_rep x) = BQ_rep (J (BZopp (P x)) (Q x)). Proof. ir. uf BQ_rep. cp (BQ_base_pr H). ee. aw. wr (BZ_gcd_opp H1 (sub_BZps_BZ H2)). set (g := BZ_gcd (P x) (Q x)). uf BQopp. aw. rww BZ_quotient_opp2. uf g. qprops. rwi inc_BZps H2. nin H2. assert (P x <> BZ_zero \/ Q x <> BZ_zero). au. cp (BZ_gcd_prop3 H1 (sub_BZp_BZ H2) H4). eee. Qed. Lemma BQ_abs_pos: forall x, inc x BQp -> BQabs x = x. Proof. ir. rwi inc_BQp_pr H. ee. uf BQabs. rww BZ_abs_pos. wrr BQ_is_graph. Qed. Lemma BQ_abs_neg: forall x, inc x BQms -> BQabs x = BQopp x. Proof. ir. rwi inc_BQms_pr H. ee. uf BQabs. rww BZ_abs_neg. Qed. Lemma BQ_stable_abs: forall a, inc a BQ -> inc (BQabs a) BQ. Proof. ir. cp H. rwi inc_BQ H0. nin H0. rw BQ_abs_neg. app BQ_stable_opp. am. rww BQ_abs_pos. Qed. Hint Resolve BQ_stable_opp BQ_stable_abs : qprops. Lemma inc_BQabs_Qp: forall x, inc x BQ -> inc (BQabs x) BQp. Proof. ir. rw inc_BQp_pr. split. qprops. qw. assert (inc (P x) BZ). app BQ_P. app inc_BZabs_N. Qed. Lemma BQopp_zero : BQopp (BQ_zero) = BQ_zero. Proof. ir. uf BQopp. qw. Qed. Lemma BQopp_positive1 : forall x, inc x BQps -> inc (BQopp x) BQms. Proof. ir. rw inc_BQms_pr. split. qprops. qw. rwi inc_BQps_pr H. ee. app BZopp_positive1. Qed. Lemma BQopp_negative1 : forall x, inc x BQms -> inc (BQopp x) BQps. Proof. ir. rw inc_BQps_pr. split. qprops. qw. rwi inc_BQms_pr H. ee. app BZopp_negative1. Qed. Lemma BQopp_positive2 : forall x, inc x BQp -> inc (BQopp x) BQm. Proof. ir. rw inc_BQm_pr. split. qprops. qw. rwi inc_BQp_pr H. ee. app BZopp_positive2. Qed. Lemma BQopp_negative2 : forall x, inc x BQm -> inc (BQopp x) BQp. Proof. ir. rw inc_BQp_pr. split. qprops. qw. rwi inc_BQm_pr H. ee. app BZopp_negative2. Qed. Lemma BQopp_inj: forall a b, inc a BQ -> inc b BQ -> BQopp a = BQopp b -> a = b. Proof. ir. cp (f_equal BQopp H1). rwi BQopp_involutive H2. rwi BQopp_involutive H2. am. am. am. Qed. Lemma BQabs_projection: forall x, inc x BQ -> BQabs (BQabs x) = BQabs x. Proof. ir. app BQ_abs_pos. app inc_BQabs_Qp. Qed. Lemma BQabs_opp: forall x, inc x BQ -> BQabs (BQopp x) = BQabs x. Proof. ir. uf BQabs. qw. rww BZabs_opp. app BQ_P. Qed. Lemma BQ_abs_zero : BQabs BQ_zero = BQ_zero. Proof. ir. app BQ_abs_pos. app inc0_BQp. Qed. Lemma BQ_abs_zero_rv : forall x, inc x BQ -> BQabs x = BQ_zero -> x = BQ_zero. Proof. ir. app BQ_zero_if_num0. cp (f_equal P H0). qwi H1. app BZ_abs_zero_rv. app BQ_P. Qed. (** ** ordering *) Definition BQ_le x y:= inc x BQ & inc y BQ & BZ_le (BZmult (P x) (Q y)) (BZmult (P y) (Q x)). Definition BQ_lt x y:= BQ_le x y & x <> y. Definition BQ_ge x y:= BQ_le y x. Definition BQ_gt x y:= BQ_lt y x. Lemma BQ_le_reflexive: forall a, inc a BQ -> BQ_le a a. Proof. ir. red. eee. app BZ_le_reflexive. cp (BQ_P H). cp (BQ_Q H). app BZ_stable_mult. Qed. Lemma BQ_order_total: forall x y, inc x BQ -> inc y BQ -> (BQ_le x y \/ BQ_le y x). Proof. ir. uf BQ_le. set (a:= (BZmult (P x) (Q y))). set (b := BZmult (P y) (Q x)). assert (inc a BZ). uf a. cp (BQ_P H). cp (BQ_Q H0). app BZ_stable_mult. assert (inc b BZ). uf b. cp (BQ_P H0). cp (BQ_Q H). app BZ_stable_mult. nin (BZ_order_total H1 H2). au. au. Qed. Lemma BQ_order_total1: forall x y, inc x BQ -> inc y BQ -> (BQ_le x y \/ BQ_lt y x). Proof. ir. nin (equal_or_not x y). rw H1. left. app BQ_le_reflexive. nin (BQ_order_total H H0). au. right. split. am. au. Qed. Lemma BQ_order_total2: forall x y, inc x BQ -> inc y BQ -> (x = y \/ BQ_lt x y \/ BQ_lt y x). Proof. ir. nin (equal_or_not x y). au. right. nin (BQ_order_total H H0). left. split. am. am. right. split. am. au. Qed. Lemma BQ_lt_pr: forall x y, BQ_lt x y = (inc x BQ & inc y BQ & BZ_lt (BZmult (P x) (Q y)) (BZmult (P y) (Q x))). Proof. ir. uf BQ_lt. app iff_eq. ir. ufi BQ_le H. eee. split. am. red. ir. assert (BQ_related x y). red. ufi BQ H. Ztac. ufi BQ H1. Ztac. eee. cp (BQ_normal_representative_unique H H1 H4). contradiction. ir. ee. nin H1. red. au. nin H1. dneg. rw H3. tv. Qed. Lemma BQ_lt_lt_trans: forall a b c, BQ_lt a b -> BQ_lt b c -> BQ_lt a c. Proof. ir. rwi BQ_lt_pr H. rwi BQ_lt_pr H0. rw BQ_lt_pr. eee. ufi BQ H. Ztac. clear H6. ufi BQ_base H5. awi H5. ufi BQ H3. Ztac. clear H7. ufi BQ_base H6. awi H6. ufi BQ H1. Ztac. clear H8. ufi BQ_base H7. awi H7. ee. assert (inc (BZmult (P a) (Q b)) BZ). app BZ_stable_mult. qprops. assert (inc (BZmult (P b) (Q a)) BZ). app BZ_stable_mult. qprops. assert (inc (BZmult (P b) (Q c)) BZ). app BZ_stable_mult. qprops. assert (inc (BZmult (P c) (Q b)) BZ). app BZ_stable_mult. qprops. cp (sub_BZps_BZ H13). cp (sub_BZps_BZ H11). cp (sub_BZps_BZ H9). rwi (BZ_prod_increasing12 H9 H14 H15) H4. rwi (BZ_prod_increasing12 H13 H16 H17) H2. rwi (BZ_mult_comm (P a) (Q b)) H4. wrii BZ_mult_assoc H4. set (u := BZmult (P a) (Q c)) in *. assert (inc u BZ). uf u. app BZ_stable_mult. rwi (BZ_mult_comm (Q b) u) H4. rwi (BZ_mult_comm (P c) (Q b)) H2. wrii BZ_mult_assoc H2. rwi (BZ_mult_comm (Q c) (Q a)) H2. rwii BZ_mult_assoc H2. assert (BZ_lt (BZmult u (Q b)) (BZmult (BZmult (Q b) (P c)) (Q a))). BZo_tac. wrii BZ_mult_assoc H22. set (v := BZmult (P c) (Q a)) in *. assert (inc v BZ). uf v. app BZ_stable_mult. rwi (BZ_mult_comm (Q b) v) H22. rww (BZ_prod_increasing12 H11 H21 H23). Qed. Lemma BQ_le_lt_trans: forall a b c, BQ_le a b -> BQ_lt b c -> BQ_lt a c. Proof. ir. nin (equal_or_not a b). ue. assert (BQ_lt a b). split; am. app (BQ_lt_lt_trans H2 H0). Qed. Lemma BQ_lt_le_trans: forall a b c, BQ_lt a b -> BQ_le b c -> BQ_lt a c. Proof. ir. nin (equal_or_not b c). ue. assert (BQ_lt b c). split; am. app (BQ_lt_lt_trans H H2). Qed. Lemma BQ_le_transitive: forall a b c, BQ_le a b -> BQ_le b c -> BQ_le a c. Proof. ir. nin (equal_or_not a b). ue. assert (BQ_lt a b). split; am. nin (BQ_lt_le_trans H2 H0). am. Qed. Lemma BQ_le_antisymmetric: forall a b, BQ_le a b -> BQ_le b a -> a=b. Proof. ir. nin (equal_or_not a b). am. assert (BQ_lt a b). split; am. assert (BQ_lt b a). split. am. au. nin (BQ_lt_lt_trans H2 H3). elim H5. tv. Qed. Definition BQ_ordering := graph_on BQ_le BQ. Lemma BQ_ordering_prop : (order BQ_ordering & total_order BQ_ordering & substrate BQ_ordering= BQ & related BQ_ordering = BQ_le). Proof. assert (order BQ_ordering). uf BQ_ordering. app order_from_rel. red. ee; red. ir. app (BQ_le_transitive H H0). ir. app (BQ_le_antisymmetric H H0). ir. split; app BQ_le_reflexive. nin H. am. red in H. eee. assert (related BQ_ordering = BQ_le). app arrow_extensionality. ir. app arrow_extensionality. ir. uf BQ_ordering. rw graph_on_rw1. uf BQ_le. ap iff_eq; ir;eee. assert (substrate BQ_ordering = BQ). app extensionality. uf BQ_ordering. app graph_on_substrate. red. ir. rw order_reflexivity. rw H0. app BQ_le_reflexive. am. eee. split. am. rw H1. ir. uf gge. uf gle. rw H0. ap (BQ_order_total H2 H3). Qed. Lemma not_BQ_le_lt: forall a b, BQ_le a b -> BQ_lt b a -> False. Proof. ir. nin H0. elim H1. ap BQ_le_antisymmetric. am. am. Qed. Ltac BQo_tac := match goal with | Ha:BQ_le ?a ?b, Hb: BQ_le ?b ?c |- BQ_le ?a ?c => ap (BQ_le_transitive Ha Hb) | Ha:BQ_lt ?a ?b, Hb: BQ_le ?b ?c |- BQ_lt ?a ?c => ap (BQ_lt_le_trans Ha Hb) | Ha:BQ_le ?a ?b, Hb: BQ_lt ?b ?c |- BQ_lt ?a ?c => ap (BQ_le_lt_trans Ha Hb) | Ha:BQ_lt ?a ?b, Hb: BQ_lt ?b ?c |- BQ_lt ?a ?c => nin Ha; BQo_tac | Ha: BQ_le ?a ?b, Hb: BQ_lt ?b ?a |- _ => elim (not_BQ_le_lt Ha Hb) | Ha:BQ_le ?x ?y, Hb: BQ_le ?y ?x |- _ => solve [ rw (BQ_le_antisymmetric Ha Hb) ; qprops ] | Ha: BQ_le ?a _ |- inc ?a BQ => nin Ha; am | Ha: BQ_le _ ?a |- inc ?a BQ => destruct Ha as [_ [Ha _ ]]; exact Ha | Ha: BQ_lt ?a _ |- inc ?a BQ => nin Ha; BQo_tac | Ha: BQ_lt _ ?a |- inc ?a BQ => nin Ha; BQo_tac end. Lemma BQ_positive_pr: forall x, BQ_le BQ_zero x = inc x BQp. Proof. ir. uf BQ_le. bw. app iff_eq. ir. ee. rw inc_BQp_pr. split. ee. am. cp (BQ_Q H0). qwii H1. wrr BZ_positive_pr. app BQ_P. ir. rwi inc_BQp_pr H. eee; qprops. qw. rww BZ_positive_pr. qprops. qprops. Qed. Lemma BQ_positive_pr1: forall x, BQ_lt BQ_zero x = inc x BQps. Proof. ir. uf BQ_lt. rw BQ_positive_pr. rw inc_BQps_pr1. ap iff_eq; ir; nin H; au. Qed. Lemma BQ_negative_pr1: forall x, BQ_le x BQ_zero = inc x BQm. Proof. ir. uf BQ_le. bw. app iff_eq. ir. ee. rw inc_BQm_pr. split. ee. am. cp (BQ_Q H). qwii H1. wrr BZ_negative_pr1. app BQ_P. ir. rwi inc_BQm_pr H. eee; qprops. qw. rww BZ_negative_pr1. qprops. qprops. Qed. Lemma BQ_negative_pr: forall x, BQ_lt x BQ_zero = inc x BQms. Proof. ir. uf BQ_lt. rw BQ_negative_pr1. sy. app inc_BQms_pr1. Qed. (** * Addition *) Definition BQplus_aux x y := J (BZplus (BZmult (P x) (Q y)) (BZmult (Q x) (P y))) (BZmult (Q x) (Q y)). Definition BQplus x y := BQ_rep (BQplus_aux x y). Lemma BQ_stable_plus0: forall x y, inc x BQ_base -> inc y BQ_base -> inc (BQplus_aux x y) BQ_base. Proof. ir. ufi BQ_base H. ufi BQ_base H0. awi H. awi H0. uf BQplus_aux. uf BQ_base. aw. ee. fprops. app BZ_stable_plus. app BZ_stable_mult. qprops. app BZ_stable_mult. qprops. app BZps_stable_mult. Qed. Lemma BQ_stable_plus1: forall x y, inc x BQ_base -> inc y BQ_base -> (BQ_related (BQplus_aux x y) (BQplus x y) & inc (BQplus x y) BQ). Proof. ir. uf BQplus. app BQ_normal_representative. app BQ_stable_plus0. Qed. Lemma BQ_stable_plus: forall x y, inc x BQ -> inc y BQ -> inc (BQplus x y) BQ. Proof. ir. ufi BQ H. Ztac. ufi BQ H0. Ztac. nin (BQ_stable_plus1 H1 H3). am. Qed. Lemma BQ_plus_comm: forall x y, BQplus x y = BQplus y x. Proof. uf BQplus. ir. uf BQplus_aux. rw (BZ_mult_comm (P y) (Q x)). rw (BZ_mult_comm (Q y) (P x)). rw (BZ_mult_comm (Q y) (Q x)). rww BZ_plus_comm. Qed. Lemma BQ_plus_compat1: forall x x' y, BQ_related x x' -> inc y BQ_base -> BQplus x y = BQplus x' y. Proof. ir. nin H. nin H1. uf BQplus. app BQ_normal_representative_unique1. red. ee. app BQ_stable_plus0. app BQ_stable_plus0. uf BQplus_aux. aw. rww (BZ_mult_comm (Q x') (P y)). set (u := (BZplus (BZmult (P x) (Q y)) (BZmult (Q x) (P y)))). set (v := (BZplus (BZmult (P x') (Q y)) (BZmult (P y) (Q x')))). ufi BQ_base H. awi H. ufi BQ_base H1. awi H1. ufi BQ_base H0. awi H0. ee. cp (sub_BZps_BZ H8). cp (sub_BZps_BZ H6). cp (sub_BZps_BZ H4). cp (BZ_stable_mult H7 H11). cp (BZ_stable_mult H9 H3). cp (BZ_stable_mult H5 H11). cp (BZ_stable_mult H3 H10). cut (BZmult u (Q x') = BZmult v (Q x)). ir. rww BZ_mult_assoc. rww BZ_mult_assoc. rww H16. uf v. app BZ_stable_plus. uf u. app BZ_stable_plus. uf u. rw BZmult_plus_distr_l. rw (BZ_mult_comm (P x) (Q y)). wrr BZ_mult_assoc. rw H2. rww BZ_mult_assoc. rw (BZ_mult_comm (Q y) (P x')). wr (BZ_mult_assoc H9 H3 H10). rw (BZ_mult_comm (Q x) (BZmult (P y) (Q x'))). wrr BZmult_plus_distr_l. am. am. am. Qed. Lemma BQ_plus_compat: forall x y x' y', BQ_related x x' -> BQ_related y y' -> BQplus x y = BQplus x' y'. Proof. ir. transitivity (BQplus x' y). app BQ_plus_compat1. nin H0; am. rw (BQ_plus_comm x' y). rw (BQ_plus_comm x' y'). app BQ_plus_compat1. nin H. nin H1. am. Qed. Lemma BQ_plus_assoc: forall x y z, inc x BQ -> inc y BQ -> inc z BQ -> BQplus x (BQplus y z) = BQplus (BQplus x y) z. Proof. ir. ufi BQ H. Ztac. ufi BQ H0. Ztac. ufi BQ H1. Ztac. nin (BQ_stable_plus1 H2 H4). cp (BQ_related_symm H8). rw (BQ_plus_compat1 H10 H6). nin (BQ_stable_plus1 H4 H6). cp (BQ_related_symm H11). rw BQ_plus_comm. rw (BQ_plus_compat1 H13 H2). uf BQplus. app BQ_normal_representative_unique1. red. ee. nin H11. nin (BQ_stable_plus1 H11 H2). nin H15. am. nin H10. nin H14. nin (BQ_stable_plus1 H14 H6). nin H16. nin H18. am. uf BQplus_aux. aw. set (u := BZmult (BZmult (Q x) (Q y)) (Q z)). ufi BQ_base H2. awi H2. ufi BQ_base H4. awi H4. ufi BQ_base H6. awi H6. ee. cp (sub_BZps_BZ H19). cp (sub_BZps_BZ H17). cp (sub_BZps_BZ H15). cp (BZ_stable_mult H16 H22). cp (BZ_stable_mult H21 H14). assert (u = BZmult (BZmult (Q y) (Q z)) (Q x)). uf u. wrr BZ_mult_assoc. rww BZ_mult_comm. wr H25. assert (forall x y, x = y -> BZmult x u = BZmult y u). ir. rww H26. app H26. rww BZmult_plus_distr_l. rww BZmult_plus_distr_l. rw BZ_plus_comm. rw BZ_plus_assoc. rw (BZ_mult_comm (BZmult (Q y) (Q z)) (P x)). rww BZ_mult_assoc. set (a:= (BZmult (BZmult (P x) (Q y)) (Q z))). rw BZ_mult_comm. rww BZ_mult_assoc. app uneq. rw BZ_mult_comm. rww BZ_mult_assoc. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. Qed. Lemma BQplus_0_l: forall x, inc x BQ -> BQplus BQ_zero x = x. Proof. ir. uf BQplus. uf BQplus_aux. set (BQ_P H). set (BQ_Q H). qw. wr (BQ_is_graph H). app BQ_rep_involutive. Qed. Lemma BQplus_0_r: forall x, inc x BQ -> BQplus x BQ_zero = x. Proof. ir. rw BQ_plus_comm. app BQplus_0_l. Qed. Hint Rewrite BQplus_0_l BQplus_0_r: qw. Lemma BQplus_opp_r: forall x, inc x BQ -> BQplus x (BQopp x) = BQ_zero. Proof. ir. uf BQplus. uf BQplus_aux. qw. cp (BQ_P H). cp (BQ_Qps H). wrr BZopp_mult_distrib_r. rw BZ_mult_comm. rww BZplus_opp_r. app BQ_zero_if_num0_bis. app BZps_stable_mult. app BZ_stable_mult. qprops. qprops. Qed. Lemma BQplus_opp_l: forall x, inc x BQ -> BQplus (BQopp x) x = BQ_zero. Proof. ir. rw BQ_plus_comm. app BQplus_opp_r. Qed. Lemma BQps_stable_plus_rl: forall x y, inc x BQps -> inc y BQps -> inc (BQplus x y) BQps. Proof. ir. rwi inc_BQps_pr H. rwi inc_BQps_pr H0. ee. uf BQplus. app BQps_stable_rep. app BQ_stable_plus0. ufi BQ H. Ztac. am. ufi BQ H0. Ztac. am. uf BQplus_aux. aw. assert (inc (BZmult (P x) (Q y)) BZps). app BZps_stable_mult. qprops. assert (inc (BZmult (Q x) (P y)) BZps). app BZps_stable_mult. qprops. app BZps_stable_plus_rl. Qed. Lemma BQ_plus_opp_distr: forall x y, inc x BQ -> inc y BQ -> BQopp (BQplus x y) = BQplus(BQopp x) (BQopp y). Proof. ir. uf BQplus. rww BQ_opp_related. app uneq. uf BQplus_aux. aw. qw. cp (BQ_P H). cp (BQ_P H0). cp (BQ_Q H0). cp (BQ_Q H). rww BZ_plus_opp_distr. rww BZopp_mult_distrib_l. rww BZopp_mult_distrib_r. app BZ_stable_mult. app BZ_stable_mult. app BQ_stable_plus0. app sub_BQbase. app sub_BQbase. Qed. Lemma BQms_stable_plus_rl: forall x y, inc x BQms -> inc y BQms -> inc (BQplus x y) BQms. Proof. ir. wr (BQopp_involutive (sub_BQms_BQ H)). wr (BQopp_involutive (sub_BQms_BQ H0)). wr BQ_plus_opp_distr. app BQopp_positive1. app BQps_stable_plus_rl. app BQopp_negative1. app BQopp_negative1. qprops. qprops. Qed. Lemma BQps_stable_plus_r: forall x y, inc x BQp -> inc y BQps -> inc (BQplus x y) BQps. Proof. ir. nin (equal_or_not x BQ_zero). rw H1. qw. qprops. app BQps_stable_plus_rl. rww inc_BQps_pr1. au. Qed. Lemma BQps_stable_plus_l: forall x y, inc x BQps -> inc y BQp -> inc (BQplus x y) BQps. Proof. ir. rw BQ_plus_comm. app BQps_stable_plus_r. Qed. Lemma BQp_stable_plus: forall x y, inc x BQp -> inc y BQp -> inc (BQplus x y) BQp. Proof. ir. nin (equal_or_not x BQ_zero). rw H1. qw. qprops. assert (inc x BQps). rww inc_BQps_pr1. au. cp (BQps_stable_plus_l H2 H0). rwi inc_BQps_pr1 H3. eee. Qed. Lemma BQms_stable_plus_r: forall x y, inc x BQm -> inc y BQms -> inc (BQplus x y) BQms. Proof. ir. nin (equal_or_not x BQ_zero). rw H1. qw. qprops. app BQms_stable_plus_rl. rww inc_BQms_pr1. au. Qed. Lemma BQms_stable_plus_l: forall x y, inc x BQms -> inc y BQm -> inc (BQplus x y) BQms. Proof. ir. rww BQ_plus_comm. app BQms_stable_plus_r. Qed. Lemma BQm_stable_plus: forall x y, inc x BQm -> inc y BQm -> inc (BQplus x y) BQm. Proof. ir. nin (equal_or_not x BQ_zero). rw H1. qw. qprops. assert (inc x BQms). rww inc_BQms_pr1. au. cp (BQms_stable_plus_l H2 H0). rwi inc_BQms_pr1 H3. eee. Qed. (** Multiplication *) Definition BQmult_aux x y := J (BZmult (P x) (P y)) (BZmult (Q x) (Q y)). Definition BQmult x y := BQ_rep (BQmult_aux x y). Lemma BQ_stable_mult0: forall x y, inc x BQ_base -> inc y BQ_base -> inc (BQmult_aux x y) BQ_base. Proof. ir. cp (BQ_base_pr H). cp (BQ_base_pr H0). ee. uf BQmult_aux. uf BQ_base. aw. ee. fprops. app BZ_stable_mult. app BZps_stable_mult. Qed. Lemma BQ_stable_mult1: forall x y, inc x BQ_base -> inc y BQ_base -> (BQ_related (BQmult_aux x y) (BQmult x y) & inc (BQmult x y) BQ). Proof. ir. uf BQmult. app BQ_normal_representative. app BQ_stable_mult0. Qed. Lemma BQ_stable_mult: forall x y, inc x BQ -> inc y BQ -> inc (BQmult x y) BQ. Proof. ir. ufi BQ H. Ztac. ufi BQ H0. Ztac. nin (BQ_stable_mult1 H1 H3). am. Qed. Lemma BQ_mult_comm: forall x y, BQmult x y = BQmult y x. Proof. uf BQmult. ir. uf BQmult_aux. rww BZ_mult_comm. rww (BZ_mult_comm (Q x) (Q y)). Qed. Lemma BQ_mult_compat1: forall x x' y, BQ_related x x' -> inc y BQ_base -> BQmult x y = BQmult x' y. Proof. ir. nin H. nin H1. uf BQmult. app BQ_normal_representative_unique1. red. ee. app BQ_stable_mult0. app BQ_stable_mult0. uf BQmult_aux. aw. ufi BQ_base H. awi H. ufi BQ_base H1. awi H1. ufi BQ_base H0. awi H0. ee. cp (sub_BZps_BZ H8). cp (sub_BZps_BZ H6). cp (sub_BZps_BZ H4). rww BZ_mult_assoc. rww BZ_mult_assoc. rw (BZ_mult_comm (P x) (P y)). wr (BZ_mult_assoc H3 H7 H10). rw H2. rww BZ_mult_assoc. rw (BZ_mult_comm (P y) (P x')). tv. app BZ_stable_mult. app BZ_stable_mult. Qed. Lemma BQ_mult_compat: forall x y x' y', BQ_related x x' -> BQ_related y y' -> BQmult x y = BQmult x' y'. Proof. ir. transitivity (BQmult x' y). app BQ_mult_compat1. nin H0; am. rw (BQ_mult_comm x' y). rw (BQ_mult_comm x' y'). app BQ_mult_compat1. nin H. nin H1. am. Qed. Lemma BQ_mult_assoc: forall x y z, inc x BQ -> inc y BQ -> inc z BQ -> BQmult x (BQmult y z) = BQmult (BQmult x y) z. Proof. ir. ufi BQ H. Ztac. ufi BQ H0. Ztac. ufi BQ H1. Ztac. nin (BQ_stable_mult1 H2 H4). cp (BQ_related_symm H8). rw (BQ_mult_compat1 H10 H6). nin (BQ_stable_mult1 H4 H6). cp (BQ_related_symm H11). rw BQ_mult_comm. rw (BQ_mult_compat1 H13 H2). uf BQmult. app BQ_normal_representative_unique1. red. ee. nin H11. nin (BQ_stable_mult1 H11 H2). nin H15. am. nin H10. nin H14. nin (BQ_stable_mult1 H14 H6). nin H16. nin H18. am. uf BQmult_aux. aw. set (u := BZmult (BZmult (Q x) (Q y)) (Q z)). ufi BQ_base H2. awi H2. ufi BQ_base H4. awi H4. ufi BQ_base H6. awi H6. ee. cp (sub_BZps_BZ H19). cp (sub_BZps_BZ H17). cp (sub_BZps_BZ H15). assert (u = BZmult (BZmult (Q y) (Q z)) (Q x)). uf u. wrr BZ_mult_assoc. rww BZ_mult_comm. wr H23. rw (BZ_mult_comm (BZmult (P y) (P z)) (P x)). rww BZ_mult_assoc. Qed. Lemma BQmult_1_l: forall x, inc x BQ -> BQmult BQ_one x = x. Proof. ir. set (BQ_P H). set (BQ_Q H). uf BQmult. uf BQmult_aux. uf BQ_one. uf BQ_of_Z. aw. qw. wr (BQ_is_graph H). app BQ_rep_involutive. Qed. Lemma BQmult_1_r: forall x, inc x BQ -> BQmult x BQ_one = x. Proof. ir. rw BQ_mult_comm. app BQmult_1_l. Qed. Lemma BQmult_0_l: forall x, inc x BQ -> BQmult BQ_zero x = BQ_zero. Proof. ir. cp (BQ_Q H). uf BQmult. uf BQmult_aux. qw. app BQ_zero_if_num0_bis. qprops. qprops. Qed. Lemma BQmult_0_r: forall x, inc x BQ -> BQmult x BQ_zero = BQ_zero. Proof. ir. rw BQ_mult_comm. app BQmult_0_l. Qed. Hint Rewrite BQmult_0_l BQmult_0_r BQmult_1_l BQmult_1_r: qw. Lemma BQmult_0_rl: forall x y, inc x BQ -> inc y BQ -> x <> BQ_zero -> y <> BQ_zero -> BQmult x y <> BQ_zero. Proof. ir. uf BQmult. app BQs_stable_rep. app BQ_stable_mult0. app sub_BQbase. app sub_BQbase. uf BQmult_aux. aw. app BZmult_0_rl. qprops. qprops. clear H2. dneg. app BQ_zero_if_num0. dneg. app BQ_zero_if_num0. Qed. Lemma BQmult_m1_l: forall x, inc x BQ -> BQmult BQ_mone x = BQopp x. Proof. ir. uf BQmult. uf BQmult_aux. uf BQ_mone. uf BQ_of_Z. aw. rww BZ_mult_m1_l. qw. change (BQ_rep (BQopp x) = BQopp x). app BQ_rep_involutive. qprops. qprops. qprops. Qed. Lemma BQmult_m1_r: forall x, inc x BQ -> BQmult x BQ_mone = BQopp x. Proof. ir. rw BQ_mult_comm. app BQmult_m1_l. Qed. Lemma BQ_opp_mone: BQopp BQ_mone = BQ_one. Proof. ir. uf BQ_mone. uf BQ_of_Z. uf BQopp. aw. qw. rww BZ_opp_mone. Qed. Lemma BQ_opp_one: BQopp BQ_one = BQ_mone. Proof. ir. wr BQ_opp_mone. app BQopp_involutive. qprops. Qed. Lemma BQopp_mult_distrib_r: forall x y, inc x BQ -> inc y BQ -> BQopp (BQmult x y) = BQmult x (BQopp y). Proof. ir. wr BQmult_m1_r. wr BQmult_m1_r. rww BQ_mult_assoc. qprops. am. app BQ_stable_mult. Qed. Lemma BQopp_mult_distrib_l: forall x y, inc x BQ -> inc y BQ -> BQopp (BQmult x y) = BQmult (BQopp x) y. Proof. ir. ir. wr BQmult_m1_l. wr BQmult_m1_l. rww BQ_mult_assoc. qprops. am. app BQ_stable_mult. Qed. Lemma BQmult_opp_comm: forall x y, inc x BQ -> inc y BQ -> BQmult x (BQopp y) = BQmult (BQopp x) y. Proof. ir. wrr BQopp_mult_distrib_l. rww BQopp_mult_distrib_r. Qed. Lemma BQmult_opp_opp: forall x y, inc x BQ -> inc y BQ -> BQmult (BQopp x) (BQopp y) = BQmult x y. Proof. ir. rw (BQmult_opp_comm (BQ_stable_opp H) H0). rww BQopp_involutive. Qed. Lemma BQps_stable_mult: forall a b, inc a BQps -> inc b BQps -> inc (BQmult a b) BQps. Proof. ir. rwi inc_BQps_pr H. rwi inc_BQps_pr H0. ee. uf BQmult. app BQps_stable_rep. app BQ_stable_mult0. ufi BQ H. Ztac. am. ufi BQ H0. Ztac. am. uf BQmult_aux. aw. app BZps_stable_mult. Qed. Lemma BQp_stable_mult: forall a b, inc a BQp -> inc b BQp -> inc (BQmult a b) BQp. Proof. ir. nin (equal_or_not a BQ_zero). rw H1. qw. qprops. uf BQ_zero. app inc_BQ_of_Zp. app inc0_BZp. qprops. nin (equal_or_not b BQ_zero). rw H2. qw. qprops. uf BQ_zero. app inc_BQ_of_Zp. app inc0_BZp. qprops. assert (inc a BQps). rw inc_BQps_pr1. au. assert (inc b BQps). rw inc_BQps_pr1. au. cp (BQps_stable_mult H3 H4). rwi inc_BQps_pr1 H5. ee. am. Qed. Lemma BQm_unstable_mult: forall a b, inc a BQm -> inc b BQm -> inc (BQmult a b) BQp. Proof. ir. wr BQmult_opp_opp. app BQp_stable_mult. app BQopp_negative2. app BQopp_negative2. qprops. qprops. Qed. Lemma BQms_unstable_mult: forall a b, inc a BQms -> inc b BQms -> inc (BQmult a b) BQps. Proof. ir. wr BQmult_opp_opp. app BQps_stable_mult. app BQopp_negative1. app BQopp_negative1. qprops. qprops. Qed. Lemma BQpm_stable_mult: forall a b, inc a BQp -> inc b BQm -> inc (BQmult a b) BQm. Proof. ir. cp (BQopp_negative2 H0). wr (BQopp_involutive (sub_BQm_BQ H0)). wr BQopp_mult_distrib_r. app BQopp_positive2. app BQp_stable_mult. qprops. qprops. Qed. Lemma BQpms_stable_mult: forall a b, inc a BQps -> inc b BQms -> inc (BQmult a b) BQms. Proof. ir. cp (BQopp_negative1 H0). wr (BQopp_involutive (sub_BQms_BQ H0)). wr BQopp_mult_distrib_r. app BQopp_positive1. app BQps_stable_mult. qprops. qprops. Qed. Lemma BQps_stable_mult1: forall a b, inc a BQ -> inc b BQ -> inc (BQmult a b) BQps -> ((inc a BQps = inc b BQps) & (inc a BQms = inc b BQms)). Proof. ir. cp H; cp H0. rwi inc_BQ1 H. nin H. rwi H H1. qwi H1. rwi inc_BQps_pr1 H1. nin H1. elim H4. tv. am. rwi inc_BQ1 H0. nin H0. rwi H0 H1. qwi H1. rwi inc_BQps_pr1 H1. nin H1. elim H4. tv. am. nin H; nin H0. split. app iff_eq. app iff_eq. ir. elim (BQ_disjoint_neg_spos H4 H). ir. elim (BQ_disjoint_neg_spos H4 H0). cp (BQpms_stable_mult H H0). elim (BQ_disjoint_neg_spos H4 H1). cp (BQpms_stable_mult H0 H). rwi BQ_mult_comm H4. elim (BQ_disjoint_neg_spos H4 H1). split. ap iff_eq. ir. elim (BQ_disjoint_neg_spos H H4). ir. elim (BQ_disjoint_neg_spos H0 H4). app iff_eq; ir. Qed. Lemma BQ_abs_neg1: forall x, inc x BQm -> BQabs x = BQopp x. Proof. ir. nin (equal_or_not x BQ_zero). rw H0. rw BQ_abs_zero. rw BQopp_zero. tv. app BQ_abs_neg. rw inc_BQms_pr1. au. Qed. Lemma BQ_mult_abs: forall x y, inc x BQ -> inc y BQ -> BQabs (BQmult x y) = BQmult (BQabs x) (BQabs y). Proof. ir. sy. rwi inc_BQ H. nin H. rww BQ_abs_neg. rwi inc_BQ H0. nin H0. rww BQ_abs_neg. rww BQ_abs_pos. rww BQmult_opp_opp. qprops. qprops. cp (BQms_unstable_mult H H0). qprops. rww BQ_abs_pos. rww BQ_abs_neg1. rww BQopp_mult_distrib_l. qprops. qprops. rw BQ_mult_comm. ap (BQpm_stable_mult H0 (sub_BQms_BQm H)). rww BQ_abs_pos. rwi inc_BQ H0. nin H0. rww BQ_abs_neg. rww BQ_abs_neg1. rww BQopp_mult_distrib_r. qprops. qprops. ap (BQpm_stable_mult H (sub_BQms_BQm H0)). rww BQ_abs_pos. rww BQ_abs_pos. app BQp_stable_mult. Qed. Theorem BQmult_plus_distr_r : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> BQmult n (BQplus m p) = BQplus (BQmult n m) (BQmult n p). Proof. ir. ufi BQ H; ufi BQ H0; ufi BQ H1. Ztac. clear H1. Ztac. clear H0. Ztac. clear H. nin (BQ_stable_mult1 H0 H1). nin (BQ_stable_mult1 H0 H2). wr (BQ_plus_compat H H7). nin (BQ_stable_plus1 H1 H2). cp (BQ_mult_compat1 H9 H0). rwi BQ_mult_comm H11. rwi (BQ_mult_comm (BQplus m p) n) H11. wr H11. uf BQmult. uf BQplus. app BQ_normal_representative_unique1. red. ee. app BQ_stable_mult0. app BQ_stable_plus0. app BQ_stable_plus0. app BQ_stable_mult0. app BQ_stable_mult0. uf BQplus_aux. uf BQmult_aux. aw. ufi BQ_base H2. awi H2. ufi BQ_base H1. awi H1. ufi BQ_base H0. awi H0. ee. cp (sub_BZps_BZ H17). cp (sub_BZps_BZ H15). cp (sub_BZps_BZ H13). set (d := BZmult (Q n) (BZmult (Q m) (Q p))). assert (inc d BZ). uf d. app BZ_stable_mult. app BZ_stable_mult. assert (inc (BZmult (P n) (Q n)) BZ). app BZ_stable_mult. assert ( BZmult (BZmult (Q n) (Q m)) (BZmult (Q n) (Q p)) = BZmult (Q n) d). rw BZ_mult_permute_2_in_4. wr BZ_mult_assoc. app uneq. am. am. app BZ_stable_mult. am. am. am. am. rw H23. rw BZ_mult_comm. rw BZ_mult_assoc. set (d1 := BZmult (BZmult (Q n) d) (P n)). set (w := BZmult d1 (BZplus (BZmult (P m) (Q p)) (BZmult (Q m) (P p)))). rww BZ_mult_permute_2_in_4. rw (BZ_mult_comm (BZmult (Q n) (Q m)) (BZmult (P n) (P p))). rww (BZ_mult_permute_2_in_4 H12 H16 H20 H19). wr BZmult_plus_distr_r. rw (BZ_mult_comm (P p) (Q m)). rw BZ_mult_comm. rww BZ_mult_assoc. rww BZ_mult_assoc. assert (d1 = BZmult (BZmult d (P n)) (Q n)). uf d1. rw (BZ_mult_comm (BZmult d (P n)) (Q n)). rww BZ_mult_assoc. wrr H24. app BZ_stable_plus. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. app BZ_stable_mult. am. app BZ_stable_plus. app BZ_stable_mult. app BZ_stable_mult. Qed. Lemma BQmult_plus_distr_l : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> BQmult (BQplus m p) n = BQplus (BQmult m n) (BQmult p n). Proof. ir. rw (BQ_mult_comm m n). rw (BQ_mult_comm p n). wrr BQmult_plus_distr_r. app BQ_mult_comm. Qed. Definition BQminus x y := BQplus x (BQopp y). Definition BQsucc x := BQplus x BQ_one. Definition BQpred x := BQminus x BQ_one. Lemma BQ_stable_minus: forall x y, inc x BQ -> inc y BQ -> inc (BQminus x y) BQ. Proof. ir. uf BQminus. app BQ_stable_plus. qprops. Qed. Lemma BQ_stable_succ: forall x, inc x BQ -> inc (BQsucc x) BQ. Proof. ir. uf BQsucc. app BQ_stable_plus. qprops. Qed. Lemma BQ_stable_pred: forall x, inc x BQ -> inc (BQpred x) BQ. Proof. ir. uf BQpred. app BQ_stable_minus. qprops. Qed. Hint Rewrite BQplus_opp_l BQplus_opp_r: qw. Hint Rewrite BQopp_zero : qw. Lemma BQ_succ_pred: forall x, inc x BQ -> BQsucc (BQpred x) = x. Proof. ir. uf BQsucc. uf BQpred. uf BQminus. wr BQ_plus_assoc. qw. qprops. am. qprops. qprops. Qed. Lemma BQ_pred_succ: forall x, inc x BQ -> BQpred (BQsucc x) = x. Proof. ir. uf BQsucc. uf BQpred. uf BQminus. wr BQ_plus_assoc. qw. qprops. am. qprops. qprops. Qed. Lemma BQminus_plus: forall n m, inc n BQ -> inc m BQ -> BQminus (BQplus n m) n = m. Proof. ir. uf BQminus. cp (BQ_stable_opp H). rww (BQ_plus_comm n m). wrr BQ_plus_assoc. qw. Qed. Lemma BQplus_minus: forall n m, inc n BQ -> inc m BQ -> BQplus n (BQminus m n) = m. Proof. ir. uf BQminus. cp (BQ_stable_opp H). rww (BQ_plus_comm m (BQopp n)). rww BQ_plus_assoc. qw. Qed. Lemma BQplus_minus_ea: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> n = BQplus m p -> p = BQminus n m. Proof. ir. rw H2. sy. app BQminus_plus. Qed. Lemma BQminus_diag: forall a, inc a BQ -> BQminus a a = BQ_zero. Proof. ir. uf BQminus. qw. Qed. Lemma BQ_minus_diag_rw: forall a b, inc a BQ -> inc b BQ -> BQminus a b = BQ_zero -> a = b. Proof. ir. cp (f_equal (BQplus b) H1). rwi BQplus_minus H2. qwi H2. am. am. am. am. Qed. Lemma BQminus_0_r: forall a, inc a BQ -> BQminus a BQ_zero = a. Proof. ir. uf BQminus. qw. Qed. Lemma BQminus_0_l: forall a, inc a BQ -> BQminus BQ_zero a = BQopp a. Proof. ir. uf BQminus. qw. qprops. Qed. Lemma BQminus_plus_simpl_l: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> BQminus (BQplus p n) (BQplus p m) = BQminus n m. Proof. ir. uf BQminus. rw BQ_plus_opp_distr. rw (BQ_plus_comm p n). cp (BQ_stable_opp H1). rww BQ_plus_assoc. wrr (BQ_plus_assoc H H1 H2). qw. app BQ_stable_plus. qprops. am. am. Qed. Lemma BQminus_plus_simpl_r: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> BQminus (BQplus n p) (BQplus m p) = BQminus n m. Proof. ir. rw (BQ_plus_comm n p). rw (BQ_plus_comm m p). app BQminus_plus_simpl_l. Qed. Lemma BQminus_plus_comm: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> BQminus (BQplus n m) p = BQplus (BQminus n p) m. Proof. ir. uf BQminus. rw (BQ_plus_comm n m). cp (BQ_stable_opp H1). wrr BQ_plus_assoc. rww BQ_plus_comm. Qed. Lemma BQminus_succ_l: forall n m, inc n BQ -> inc m BQ -> BQsucc (BQminus n m) = BQminus (BQsucc n) m. Proof. ir. uf BQsucc. sy. app BQminus_plus_comm. qprops. Qed. Lemma BQplus_reg_r : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> BQplus m n = BQplus p n -> m = p. Proof. ir. wr (BQminus_plus H H0). rww BQ_plus_comm. rww H2. rww BQ_plus_comm. app BQminus_plus. Qed. Lemma BQplus_reg_l : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> BQplus n m = BQplus n p -> m = p. Proof. ir. rwi BQ_plus_comm H2. rwi (BQ_plus_comm n p) H2. app (BQplus_reg_r H H0 H1 H2). Qed. Lemma BQmult_minus_distr_r : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> BQmult n (BQminus m p) = BQminus (BQmult n m) (BQmult n p). Proof. uf BQminus. ir. rww BQmult_plus_distr_r. wrr BQopp_mult_distrib_r. qprops. Qed. Lemma BQmult_minus_distr_l : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> BQmult (BQminus m p) n = BQminus (BQmult m n) (BQmult p n). Proof. ir. rww (BQ_mult_comm m n). rww (BQ_mult_comm p n). wrr BQmult_minus_distr_r. app BQ_mult_comm. Qed. Lemma BQ_minus_inj: forall a b, inc a BQ -> inc b BQ -> BQminus a b = BQ_zero -> a = b. Proof. ir. cp (BQplus_minus H0 H). rwi H1 H2. qwi H2. sy; am. am. Qed. Lemma BQmult_reg_r : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> n <> BQ_zero -> BQmult m n = BQmult p n -> m=p. Proof. ir. cp (BQmult_minus_distr_l H H0 H1). rwi H3 H4. rwi BQminus_diag H4. nin (equal_or_not (BQminus m p) BQ_zero). app BQ_minus_inj. cp (BQmult_0_rl (BQ_stable_minus H0 H1) H H5 H2). contradiction. app BQ_stable_mult. Qed. Lemma BQmult_reg_l : forall n m p, inc n BQ -> inc m BQ -> inc p BQ -> n <> BQ_zero -> BQmult n m = BQmult n p -> m=p. Proof. ir. rwi (BQ_mult_comm n m) H3. rwi (BQ_mult_comm n p) H3. ap (BQmult_reg_r H H0 H1 H2 H3). Qed. Lemma BQplus_diag_eq_mult_2: forall n, inc n BQ -> BQplus n n = BQmult n BQ_two. Proof. ir. cp (sub_BQbase H). cp (BQ_base_pr H0). ee. cp (sub_BZps_BZ H3). uf BQmult. uf BQplus. app BQ_normal_representative_unique1. red. ee. app BQ_stable_plus0. app BQ_stable_mult0. app sub_BQbase. qprops. uf BQplus_aux. uf BQmult_aux. uf BQ_two. uf BQ_of_Z. aw. qw. assert (inc (BZmult (P n) (Q n)) BZ). app BZ_stable_mult. cp (inc2_BZ). rw (BZ_mult_comm (Q n) (P n)). rww (BZplus_diag_eq_mult_2). rww BZ_mult_permute_2_in_4. rww BZ_mult_assoc. Qed. Lemma BQmult_succ_r : forall n m, inc n BQ -> inc m BQ -> BQmult n (BQsucc m) = BQplus (BQmult n m) n. Proof. ir. uf BQsucc. rww BQmult_plus_distr_r. qw. qprops. Qed. Lemma BQmult_succ_l : forall n m, inc n BQ -> inc m BQ -> BQmult (BQsucc n) m = BQplus (BQmult n m) m. Proof. ir. rww BQ_mult_comm. rw (BQ_mult_comm n m). rww BQmult_succ_r. Qed. (** The sign function *) Definition BQsign x:= BQ_of_Z (BZsign (P x)). Lemma BQ_stable_sign: forall x, inc (BQsign x) BQ. Proof. ir. uf BQsign. app inc_BQ_of_Z. qprops. Qed. Hint Resolve BQ_stable_sign: qprops. Lemma BQ_sign_pos: forall x, inc x BQps -> BQsign x = BQ_one. Proof. ir. uf BQsign. rww BZ_sign_pos. rwi inc_BQps_pr H. ee; am. Qed. Lemma BQ_sign_neg: forall x, inc x BQms -> BQsign x = BQ_mone. Proof. ir. uf BQsign. rww BZ_sign_neg. rwi inc_BQms_pr H. ee; am. Qed. Lemma BQ_sign_zero: BQsign BQ_zero = BQ_zero. Proof. uf BQsign. qw. rww BZ_sign_zero. Qed. Lemma BQ_abs_sign: forall x, inc x BQ -> x = BQmult (BQsign x) (BQabs x). Proof. ir. cp (BQ_stable_abs H). rwi inc_BQ1 H. nin H. rw H. rw BQ_sign_zero. qw. ue. nin H. rww BQ_sign_pos. qw. rww BQ_abs_pos. app sub_BQps_BQp. rww BQ_sign_neg. rww BQmult_m1_l. rww BQ_abs_neg. rww BQopp_involutive. qprops. Qed. Lemma BQ_sign_abs: forall x, inc x BQ -> BQmult x (BQsign x) = (BQabs x). Proof. ir. cp H. cp (BQ_stable_sign x). rwi inc_BQ1 H. nin H. rw H. rw BQ_abs_zero. qw. ue. nin H. rww BQ_sign_pos. qw. rww BQ_abs_pos. app sub_BQps_BQp. rww BQ_sign_neg. rww BQmult_m1_r. rww BQ_abs_neg. Qed. Lemma BQ_sign_trichotomy: forall a, inc a BQ -> BQsign a = BQ_one \/ BQsign a = BQ_mone \/ BQsign a = BQ_zero. Proof. ir. rwi inc_BQ1 H. nin H. rw H. rw BQ_sign_zero. au. nin H. rww BQ_sign_pos. au. rww BQ_sign_neg. au. Qed. Lemma BQ_opp_sign: forall x, inc x BQ -> BQsign (BQopp x) = BQopp (BQsign x). Proof. ir. rwi inc_BQ1 H. nin H. rw H. qw. rw BQ_sign_zero. qw. nin H. rww BQ_sign_neg. rww BQ_sign_pos. rww BQ_opp_one. app BQopp_positive1. rww BQ_sign_pos. rww BQ_sign_neg. rww BQ_opp_mone. app BQopp_negative1. Qed. Lemma BQ_mult_sign: forall x y, inc x BQ -> inc y BQ -> BQsign (BQmult x y) = BQmult (BQsign x) (BQsign y). Proof. assert (forall x y, inc x BQps -> inc y BQ -> BQsign (BQmult x y) = BQmult (BQsign x) (BQsign y)). ir. rw (BQ_sign_pos H). qw. rwi inc_BQ1 H0. nin H0. rw H0. qw. qprops. nin H0. rww BQ_sign_pos. rww BQ_sign_pos. app BQps_stable_mult. rww BQ_sign_neg. rww BQ_sign_neg. app BQpms_stable_mult. qprops. ir. rwi inc_BQ1 H0. nin H0. rw H0. rww BQ_sign_zero. qw. rww BQ_sign_zero. qprops. nin H0. app H. cp (BQopp_negative1 H0). cp (sub_BQps_BQ H2). set (rhs := BQmult (BQsign x) (BQsign y)). wr (BQopp_involutive (sub_BQms_BQ H0)). cp (BQ_stable_sign x). wrr BQopp_mult_distrib_l. rw BQ_opp_sign. rww H. rw BQ_opp_sign. rww BQopp_mult_distrib_l. rww (BQopp_involutive H4). qprops. qprops. qprops. app BQ_stable_mult. Qed. Lemma BQ_lt_minus: forall a b, inc a BQ -> inc b BQ -> (BQ_lt a b = inc (BQminus b a) BQps). Proof. ir. uf BQ_lt. uf BQ_le. cp (sub_BQbase H). cp (sub_BQbase H0). cp (BQ_base_pr H1). cp (BQ_base_pr H2). ee. assert (inc (BZmult (P b) (Q a)) BZ). app BZ_stable_mult. qprops. assert (inc (BZmult (P a) (Q b)) BZ). app BZ_stable_mult. qprops. rww BZ_le_minus. set (t := BZminus (BZmult (P b) (Q a)) (BZmult (P a) (Q b))). assert (BQminus b a = BQ_rep (J t (BZmult (Q b) (Q a)))). uf BQminus. uf BQplus. uf BQplus_aux. uf BQopp. aw. assert (t = BZplus (BZmult (P b) (Q a)) (BZmult (Q b) (BZopp (P a)))). uf t. wr BZopp_mult_distrib_r. uf BZminus. rww (BZ_mult_comm (Q b) (P a)). qprops. am. ue. set (d := BZmult (Q b) (Q a)) in H11. ufi BQ_rep H11. awi H11. rw inc_BQps_pr. assert (P (BQminus b a) = (BZquo t (BZ_gcd t d))). rw H11. aw. rw H12. assert (inc t BZ). uf t. app BZ_stable_minus. assert (inc d BZ). uf d. app BZ_stable_mult. qprops. qprops. assert (inc (BZ_gcd t d) BZp). qprops. ap iff_eq. ir. ee. app BQ_stable_minus. rw inc_BZps. split. app BZp_stable_quo. app BZ_non_zero_quo_gcd. dneg. app BQ_normal_representative_unique. red. ee. am. am. sy. app BZ_minus_diag_rw. ir. cp (BZ_gcd_diva H13 H14). ee. am. am. rw H17. app BZp_stable_mult. qprops. red. ir. rwi H19 H12. rwi BQminus_diag H12. assert ( (BZquo t (BZ_gcd t d)) <> BZ_zero). rwi inc_BZps H18. ee. am. qwi H12. elim H20. au. am. Qed. Lemma BQ_le_lt_equiv: forall a b, BQ_le a b = (BQ_lt a b \/ (inc a BQ & a =b)). Proof. ir. uf BQ_lt. ap iff_eq. ir. nin (equal_or_not a b). right. nin H. au. au. ir. nin H. nin H. am. nin H. wr H0. app BQ_le_reflexive. Qed. Lemma BQ_le_minus: forall a b, inc a BQ -> inc b BQ -> (BQ_le a b = inc (BQminus b a) BQp). Proof. ir. rw BQ_le_lt_equiv. rww BQ_lt_minus. rw inc_BQps_pr1. app iff_eq. ir. nin H1; nin H1. am. rw H2. rww BQminus_diag. app inc0_BQp. ir. nin (equal_or_not b a). au. left. split. am. dneg. app BQ_minus_inj. Qed. Lemma BQ_le_minus1: forall a b, inc a BQ -> inc b BQ -> (BQ_le a b = BQ_le BQ_zero (BQminus b a)). Proof. ir. rww BQ_le_minus. rww BQ_positive_pr. Qed. Lemma BQ_lt_minus1: forall a b, inc a BQ -> inc b BQ -> (BQ_lt a b = BQ_lt BQ_zero (BQminus b a)). Proof. ir. rww BQ_lt_minus. rww BQ_positive_pr1. Qed. Lemma BQ_opp_minus: forall a b, inc a BQ -> inc b BQ -> BQopp (BQminus a b) = BQminus b a. Proof. ir. uf BQminus. rww BQ_plus_opp_distr. rww BQopp_involutive. app BQ_plus_comm. qprops. Qed. Lemma BQ_lt_minus2: forall a b, inc a BQ -> inc b BQ -> (BQ_lt a b = inc (BQminus a b) BQms). Proof. ir. rww BQ_lt_minus. wr (BQ_opp_minus H0 H). set (c:= (BQminus b a)). assert (inc c BQ). uf c. app BQ_stable_minus. app iff_eq. ir. app BQopp_positive1. ir. cp (BQopp_negative1 H2). rwi BQopp_involutive H3. am. am. Qed. Lemma BQ_sum_increasing_left: forall a b c, inc a BQ -> inc b BQ -> inc c BQ -> (BQ_le a b = BQ_le (BQplus c a) (BQplus c b)). Proof. ir. rww BQ_le_minus. cp (BQ_stable_plus H1 H). cp (BQ_stable_plus H1 H0). rww BQ_le_minus. uf BQminus. rww (BQ_plus_opp_distr H1 H). rw (BQ_plus_comm c b). cp (BQ_stable_opp H). cp (BQ_stable_opp H1). rww BQ_plus_assoc. wr (BQ_plus_assoc H0 H1 H5). qw. app BQ_stable_plus. Qed. Lemma BQ_sum_increasing_right: forall a b c, inc a BQ -> inc b BQ -> inc c BQ -> (BQ_le a b = BQ_le (BQplus a c) (BQplus b c)). Proof. ir. rw (BQ_plus_comm a c). rw (BQ_plus_comm b c). app BQ_sum_increasing_left. Qed. Lemma BQ_sum_strict_increasing_left: forall a b c, inc a BQ -> inc b BQ -> inc c BQ -> (BQ_lt a b = BQ_lt (BQplus c a) (BQplus c b)). Proof. ir. rww BQ_lt_minus. cp (BQ_stable_plus H1 H). cp (BQ_stable_plus H1 H0). rww BQ_lt_minus. uf BQminus. rww (BQ_plus_opp_distr H1 H). rw (BQ_plus_comm c b). cp (BQ_stable_opp H). cp (BQ_stable_opp H1). rww BQ_plus_assoc. wr (BQ_plus_assoc H0 H1 H5). qw. app BQ_stable_plus. Qed. Lemma BQ_sum_strict_increasing_right: forall a b c, inc a BQ -> inc b BQ -> inc c BQ -> (BQ_lt a b = BQ_lt (BQplus a c) (BQplus b c)). Proof. ir. rw (BQ_plus_comm a c). rw (BQ_plus_comm b c). app BQ_sum_strict_increasing_left. Qed. Lemma BQ_le_opp: forall x y, BQ_le x y -> BQ_le (BQopp y) (BQopp x). Proof. ir. uf BQ_le. qw. red in H. ee. qprops. qprops. wr BZopp_mult_distrib_l;qprops. wr BZopp_mult_distrib_l;qprops. app BZ_le_opp. Qed. Lemma BQ_lt_opp: forall x y, BQ_lt x y -> BQ_lt (BQopp y) (BQopp x). Proof. ir. nin H. red. split. app BQ_le_opp. dneg. red in H. ee. sy. app BQopp_inj. Qed. Lemma BQ_lt_opp1: forall x y, inc x BQ -> inc y BQ -> BQ_lt x y = BQ_lt (BQopp y) (BQopp x). Proof. ir. app iff_eq. ir. app BQ_lt_opp. ir. wrr (BQopp_involutive H). wrr (BQopp_involutive H0). app BQ_lt_opp. Qed. Lemma BQ_sum_increasing0: forall a b c d, BQ_le a c -> BQ_le b d -> BQ_le (BQplus a b) (BQplus c d). Proof. ir. assert (inc a BQ). BQo_tac. assert (inc c BQ). BQo_tac. assert (inc b BQ). BQo_tac. assert (inc d BQ). BQo_tac. assert (BQ_le (BQplus a b) (BQplus a d)). wrr BQ_sum_increasing_left. assert (BQ_le (BQplus a d) (BQplus c d)). wrr BQ_sum_increasing_right. BQo_tac. Qed. Lemma BQ_sum_increasing1: forall a b c d, BQ_le a c -> BQ_lt b d -> BQ_lt (BQplus a b) (BQplus c d). Proof. ir. assert (inc a BQ). BQo_tac. assert (inc c BQ). BQo_tac. assert (inc b BQ). nin H0. BQo_tac. assert (inc d BQ). nin H0. BQo_tac. assert (BQ_lt (BQplus a b) (BQplus a d)). wrr BQ_sum_strict_increasing_left. assert (BQ_le (BQplus a d) (BQplus c d)). wrr BQ_sum_increasing_right. BQo_tac. Qed. Lemma BQ_sum_increasing2: forall a b c d, BQ_lt a c -> BQ_le b d -> BQ_lt (BQplus a b) (BQplus c d). Proof. ir. rw BQ_plus_comm. rw (BQ_plus_comm c d). app BQ_sum_increasing1. Qed. Lemma BQ_sum_increasing3: forall a b c d, BQ_lt a c -> BQ_lt b d -> BQ_lt (BQplus a b) (BQplus c d). Proof. ir. nin H. app BQ_sum_increasing1. Qed. Lemma BQ_sum_increasing4: forall a c d, BQ_le a c -> BQ_le BQ_zero d -> BQ_le a (BQplus c d). Proof. ir. cp (BQ_sum_increasing0 H H0). qwi H1. am. BQo_tac. Qed. Lemma BQ_sum_increasing5: forall a c d, BQ_le a c -> BQ_lt BQ_zero d -> BQ_lt a (BQplus c d). Proof. ir. cp (BQ_sum_increasing1 H H0). qwi H1. am. BQo_tac. Qed. Lemma BQ_sum_increasing6: forall a c d, BQ_lt a c -> BQ_le BQ_zero d -> BQ_lt a (BQplus c d). Proof. ir. cp (BQ_sum_increasing2 H H0). qwi H1. am. nin H. BQo_tac. Qed. Lemma BQ_sum_increasing7: forall a c d, BQ_lt a c -> BQ_lt BQ_zero d -> BQ_lt a (BQplus c d). Proof. ir. cp (BQ_sum_increasing3 H H0). qwi H1. am. nin H. BQo_tac. Qed. Lemma BQ_sum_increasing8: forall a b c , BQ_le a c -> BQ_le b BQ_zero -> BQ_le (BQplus a b) c. Proof. ir. cp (BQ_sum_increasing0 H H0). qwi H1. am. BQo_tac. Qed. Lemma BQ_sum_increasing9: forall a b c, BQ_le a c -> BQ_lt b BQ_zero -> BQ_lt (BQplus a b) c. Proof. ir. cp (BQ_sum_increasing1 H H0). qwi H1. am. BQo_tac. Qed. Lemma BQ_sum_increasing10: forall a b c, BQ_lt a c -> BQ_le b BQ_zero -> BQ_lt (BQplus a b) c. Proof. ir. cp (BQ_sum_increasing2 H H0). qwi H1. am. nin H. BQo_tac. Qed. Lemma BQ_sum_increasing12: forall a b c, BQ_lt a c -> BQ_lt b BQ_zero -> BQ_lt (BQplus a b) c. Proof. ir. cp (BQ_sum_increasing3 H H0). qwi H1. am. nin H. BQo_tac. Qed. Lemma BQ_sum_increasing13: forall a b, inc a BQ -> inc b BQp -> BQ_le a (BQplus a b). Proof. ir. wri BQ_positive_pr H0. cp (BQ_le_reflexive H). app BQ_sum_increasing4. Qed. Lemma BQ_sum_increasing14: forall a b, inc a BQ -> inc b BQps -> BQ_lt a (BQplus a b). Proof. ir. wri BQ_positive_pr1 H0. cp (BQ_le_reflexive H). app BQ_sum_increasing5. Qed. Lemma BQ_sum_increasing15: forall a b, inc a BQ -> inc b BQm -> BQ_le (BQplus a b) a. Proof. ir. wri BQ_negative_pr1 H0. cp (BQ_le_reflexive H). app BQ_sum_increasing8. Qed. Lemma BQ_sum_increasing16: forall a b, inc a BQ -> inc b BQms -> BQ_lt (BQplus a b) a. Proof. ir. wri BQ_negative_pr H0. cp (BQ_le_reflexive H). app BQ_sum_increasing9. Qed. Lemma BQ_one_not_zero: BQ_one <> BQ_zero. Proof. uf BQ_one. uf BQ_zero. red. ir. cp (BQ_of_Z_inj inc1_BZ inc0_BZ H). elim BZ_one_not_zero. am. Qed. Lemma inc1_BQs: inc BQ_one BQps. Proof. rw inc_BQps_pr1. split. app inc1_BQp. ap BQ_one_not_zero. Qed. Lemma BQ_lt_succ: forall n, inc n BQ -> BQ_lt n (BQsucc n). Proof. ir. uf BQsucc. cp inc1_BQ. rww BQ_lt_minus. uf BQsucc. rww BQminus_plus. ap inc1_BQs. app BQ_stable_plus. Qed. Lemma BQ_lt_pred: forall n, inc n BQ -> BQ_lt (BQpred n) n. Proof. ir. assert (inc (BQpred n) BQ). uf BQpred. app BQ_stable_minus. qprops. wr (BQ_succ_pred H). rww BQ_pred_succ. app BQ_lt_succ. Qed. Lemma BQ_compare_opp_pos: forall x, inc x BQp -> BQ_le (BQopp x) x. Proof. ir. cp (BQopp_positive2 H). wri BQ_positive_pr H. wri BQ_negative_pr1 H0. BQo_tac. Qed. Lemma BQ_compare_opp_neg: forall x, inc x BQms -> BQ_le x (BQopp x). Proof. ir. cp (BQopp_negative1 H). wri BQ_positive_pr1 H0. wri BQ_negative_pr H. nin H; nin H0. BQo_tac. Qed. Lemma BQ_le_abs: forall n, inc n BQ -> BQ_le n (BQabs n). Proof. ir. cp H. rwi inc_BQ H. nin H. rww BQ_abs_neg. app BQ_compare_opp_neg. rww BQ_abs_pos. app BQ_le_reflexive. Qed. Lemma BQ_le_triangular: forall n m, inc n BQ -> inc m BQ -> BQ_le (BQabs (BQplus n m)) (BQplus (BQabs n) (BQabs m)). Proof. assert (forall n m, inc n BQp -> inc m BQp -> BQ_le (BQabs (BQplus n m)) (BQplus (BQabs n) (BQabs m))). ir. rw (BQ_abs_pos H). rw (BQ_abs_pos H0). cp (BQp_stable_plus H H0). rw (BQ_abs_pos H1). app BQ_le_reflexive. qprops. assert (forall n m, inc n BQp -> inc m BQ -> BQ_le (BQabs (BQplus n m)) (BQplus (BQabs n) (BQabs m))). ir. cp H1. cp (sub_BQp_BQ H0). rwi inc_BQ H1. nin H1. rw (BQ_abs_pos H0). rw (BQ_abs_neg H1). cp (BQ_stable_opp H2). assert (inc (BQplus n m) BQ). app BQ_stable_plus. rwi inc_BQ H5. nin H5. rw (BQ_abs_neg H5). rww BQ_plus_opp_distr. wrr BQ_sum_increasing_right. app BQ_compare_opp_pos. qprops. rww (BQ_abs_pos H5). wrr BQ_sum_increasing_left. app BQ_compare_opp_neg. app H. ir. rwi inc_BQ H1. nin H1. cp (sub_BQms_BQ H1). cp (BQ_stable_plus H3 H2). cp (H0 _ _ (sub_BQps_BQp (BQopp_negative1 H1)) (BQ_stable_opp H2)). wri BQ_plus_opp_distr H5. do 3 rwi BQabs_opp H5; try am. am. am. app H0. Qed. Lemma BQ_prod_increasing1: forall a b c, inc c BQp -> BQ_le a b -> BQ_le (BQmult a c) (BQmult b c). Proof. ir. assert (inc a BQ). BQo_tac. assert (inc b BQ). BQo_tac. cp (sub_BQp_BQ H). rw BQ_le_minus; try app BQ_stable_mult. wrr BQmult_minus_distr_l. app BQp_stable_mult. wrr BQ_le_minus. Qed. Lemma BQ_prod_increasing2: forall a b c, inc c BQps -> BQ_lt a b -> BQ_lt (BQmult a c) (BQmult b c). Proof. ir. cp (sub_BQps_BQ H). assert (inc a BQ). nin H0; BQo_tac. assert (inc b BQ). nin H0. BQo_tac. rw BQ_lt_minus. wrr BQmult_minus_distr_l. app BQps_stable_mult. wrr BQ_lt_minus. app BQ_stable_mult. app BQ_stable_mult. Qed. Lemma BQ_prod_increasing3: forall a b c, inc c BQm -> BQ_le a b -> BQ_ge (BQmult a c) (BQmult b c). Proof. ir. cp (sub_BQm_BQ H). assert (inc a BQ). BQo_tac. assert (inc b BQ). BQo_tac. uf BQ_ge. rw BQ_le_minus. wrr BQmult_minus_distr_l. app BQm_unstable_mult. wrr BQ_opp_minus. app BQopp_positive2. wrr BQ_le_minus. app BQ_stable_mult. app BQ_stable_mult. Qed. Lemma BQ_prod_increasing4: forall a b c, inc c BQms -> BQ_lt a b -> BQ_gt (BQmult a c) (BQmult b c). Proof. ir. cp (sub_BQms_BQ H). assert (inc a BQ). nin H0; BQo_tac. assert (inc b BQ). nin H0. BQo_tac. uf BQ_gt. rw BQ_lt_minus. wrr BQmult_minus_distr_l. app BQms_unstable_mult. wrr BQ_opp_minus. app BQopp_positive1. wrr BQ_lt_minus. app BQ_stable_mult. app BQ_stable_mult. Qed. Lemma BQ_prod_increasing5: forall a b c d, inc b BQp -> inc c BQp -> BQ_le a b -> BQ_le c d -> BQ_le (BQmult a c) (BQmult b d). Proof. ir. cp (BQ_prod_increasing1 H0 H1). cp (BQ_prod_increasing1 H H2). rwi BQ_mult_comm H4. rwi (BQ_mult_comm d b) H4. BQo_tac. Qed. Lemma BQ_prod_increasing6: forall a b c d, inc b BQps -> inc c BQps -> BQ_lt a b -> BQ_lt c d -> BQ_lt (BQmult a c) (BQmult b d). Proof. ir. cp (BQ_prod_increasing2 H0 H1). cp (BQ_prod_increasing2 H H2). rwi BQ_mult_comm H4. rwi (BQ_mult_comm d b) H4. BQo_tac. Qed. Lemma BQ_prod_increasing7: forall a b c d, inc a BQp -> inc c BQp -> BQ_lt a b -> BQ_lt c d -> BQ_lt (BQmult a c) (BQmult b d). Proof. assert (forall a b, inc a BQp -> BQ_lt a b -> inc b BQps). ir. wri BQ_positive_pr H. wr BQ_positive_pr1. BQo_tac. ir. cp (H _ _ H0 H2). cp (H _ _ H1 H3). nin (equal_or_not c BQ_zero). rw H6. qw. rw BQ_positive_pr1. app BQps_stable_mult. qprops. app BQ_prod_increasing6. rw inc_BQps_pr1. au. Qed. Lemma BQ_prod_increasing8: forall a b c, inc b BQp -> BQ_le a b -> BQ_le BQ_one c -> BQ_le a (BQmult b c). Proof. ir. cp (BQ_prod_increasing5 H inc1_BQp H0 H1). qwi H2. am. BQo_tac. Qed. Lemma BQ_prod_increasing9: forall a c, inc a BQp -> BQ_le BQ_one c -> BQ_le a (BQmult a c). Proof. ir. cp (BQ_le_reflexive (sub_BQp_BQ H)). ap (BQ_prod_increasing8 H H1 H0). Qed. Lemma BQ_prod_increasing10: forall a b c, inc b BQp -> BQ_le BQ_one c -> BQ_lt a b -> BQ_lt a (BQmult b c). Proof. ir. nin (equal_or_not BQ_one c). wr H2. qw. qprops. assert (BQ_lt BQ_one c). split; au. assert (inc a BQ). BQo_tac. cp H4. rwi inc_BQ H5. nin H5. wri BQ_negative_pr H5. cp inc1_BQp. wri BQ_positive_pr H6. assert (BQ_le BQ_zero c). BQo_tac. rwi BQ_positive_pr H7. cp (BQp_stable_mult H H7). wri BQ_positive_pr H8. BQo_tac. cp (BQ_prod_increasing7 H5 inc1_BQp H1 H3). qwi H6. am. am. Qed. Lemma BQ_prod_increasing11: forall a b c, inc c BQps -> inc a BQ -> inc b BQ -> BQ_le a b = BQ_le (BQmult a c) (BQmult b c). Proof. ir. assert (inc c BQp). rwi inc_BQps_pr1 H. nin H. am. assert (inc c BQ). qprops. rww BQ_le_minus. rww BQ_le_minus; try app BQ_stable_mult. wrr BQmult_minus_distr_l. set (d := BQminus b a). ap iff_eq. ir. app BQp_stable_mult. ir. assert (inc d BQ). uf d. app BQ_stable_minus. rwi inc_BQ H5. nin H5. cp (BQpms_stable_mult H H5). rwi BQ_mult_comm H6. elim (BQ_disjoint_neg_pos H6 H4). am. Qed. Lemma BQ_prod_increasing12: forall a b c, inc c BQps -> inc a BQ -> inc b BQ -> BQ_lt a b = BQ_lt (BQmult a c) (BQmult b c). Proof. ir. assert (inc c BQ). qprops. rww BQ_lt_minus. rww BQ_lt_minus;try app BQ_stable_mult. wrr BQmult_minus_distr_l. set (d := BQminus b a). ap iff_eq. ir. app BQps_stable_mult. ir. assert (inc d BQ). uf d. app BQ_stable_minus. rwi inc_BQ1 H4. nin H4. rwi H4 H3. qwi H3. rwi inc_BQps_pr1 H3. ee. elim H5. tv. am. nin H4. am. cp (BQpms_stable_mult H H4). rwi BQ_mult_comm H5. elim (BQ_disjoint_neg_spos H5 H3). Qed. Lemma BQ_mult_permute_2_in_4: forall a b c d, inc a BQ -> inc b BQ -> inc c BQ -> inc d BQ -> BQmult (BQmult a b) (BQmult c d) = BQmult (BQmult a c) (BQmult b d). Proof. ir. rw BQ_mult_assoc. rw BQ_mult_assoc. cut (BQmult (BQmult a b) c = (BQmult (BQmult a c) b)). ir. rww H3. wrr BQ_mult_assoc. wr BQ_mult_assoc. rw (BQ_mult_comm b c). tv. am. am. am. app BQ_stable_mult. am. am. app BQ_stable_mult. am. am. Qed. Lemma BQ_plus_permute_2_in_4: forall a b c d, inc a BQ -> inc b BQ -> inc c BQ -> inc d BQ -> BQplus (BQplus a b) (BQplus c d) = BQplus (BQplus a c) (BQplus b d). Proof. ir. rw BQ_plus_assoc. rw BQ_plus_assoc. cut (BQplus (BQplus a b) c = (BQplus (BQplus a c) b)). ir. rww H3. wr BQ_plus_assoc. wr BQ_plus_assoc. rw (BQ_plus_comm b c). tv. am. am. am. am. am. am. app BQ_stable_plus. am. am. app BQ_stable_plus. am. am. Qed. (** ** Division *) Definition BQinv x := Yo (inc x BQps) (J (Q x) (P x)) (Yo (inc x BQms) (J (BZopp (Q x)) (BZopp (P x))) BQ_zero). Definition BQdiv x y := BQmult x (BQinv y). Lemma BQ_inv_0 : BQinv BQ_zero = BQ_zero. Proof. uf BQinv. rww Y_if_not_rw. rww Y_if_not_rw. red. ir. ap (BQ_disjoint_neg_0 H (refl_equal BQ_zero)). red. ir. ap (BQ_disjoint_pos_0 H (refl_equal BQ_zero)). Qed. Lemma BQ_inv_pos: forall x, inc x BQps -> BQinv x = J (Q x) (P x). Proof. ir. uf BQinv. rww Y_if_rw. Qed. Lemma BQ_inv_neg: forall x, inc x BQms -> BQinv x = J (BZopp (Q x)) (BZopp (P x)). Proof. ir. uf BQinv. rww Y_if_not_rw. rww Y_if_rw. red. ir. elim (BQ_disjoint_neg_spos H H0). Qed. Lemma BQ_stable_inv: forall x, inc (BQinv x) BQ. Proof. ir. uf BQinv. nin (inc_or_not x BQps). rww Y_if_rw. rwi inc_BQps_pr H. ee. cp (BQ_Q H). ufi BQ H. Ztac. uf BQ. clear H. Ztac. uf BQ_base. aw. split. ee. fprops. ee. qprops. am. aw. red. rww BZ_gcd_comm. qprops. rww Y_if_not_rw. nin (inc_or_not x BQms). rww Y_if_rw. rwi inc_BQms_pr H0. ee. cp (BQ_Q H0). ufi BQ H0. Ztac. uf BQ. clear H0. Ztac. uf BQ_base. aw. split. ee. fprops. ee. qprops. app BZopp_negative1. aw. red. wrr BZ_gcd_opp. rww BZ_gcd_comm. wrr BZ_gcd_opp. qprops. qprops. qprops. rww Y_if_not_rw. qprops. Qed. Lemma BQ_mult_inv_r: forall x, inc x BQ -> x <> BQ_zero -> BQmult x (BQinv x) = BQ_one. Proof. ir. assert (forall u, inc u BZps -> BQ_rep (J u u) = BQ_one). ir. wr (BQ_rep_involutive inc1_BQ). app BQ_normal_representative_unique1. red. ee. uf BQ_base. aw. ee. fprops. qprops. am. app sub_BQbase. qprops. uf BQ_one. uf BQ_of_Z. aw. rww BZ_mult_comm. cp H. rwi inc_BQ1 H. nin H. contradiction. nin H. rw BQ_inv_pos. uf BQmult. uf BQmult_aux. aw. rww BZ_mult_comm. app H1. app BZps_stable_mult. app (BQ_Qps H2). rwi inc_BQps_pr H. eee. am. rww BQ_inv_neg. uf BQmult. uf BQmult_aux. aw. cp (BQ_P H2). cp (BQ_Q H2). rww BZmult_opp_comm. rww BZ_mult_comm. app H1. app BZps_stable_mult. app (BQ_Qps H2). rwi inc_BQms_pr H. nin H. app BZopp_negative1. Qed. Lemma BQ_mult_inv_l: forall x, inc x BQ -> x <> BQ_zero -> BQmult (BQinv x) x = BQ_one. Proof. ir. rw BQ_mult_comm. app BQ_mult_inv_r. Qed. Lemma BQ_inv_pr_r: forall x y, inc x BQ -> inc y BQ -> BQmult x y = BQ_one -> y = BQinv x. Proof. ir. nin (equal_or_not x BQ_zero). rwi H2 H1. qwi H1. elim BQ_one_not_zero. sy; am. am. cp (BQ_mult_inv_r H H2). wri H3 H1. app (BQmult_reg_l H H0 (BQ_stable_inv x) H2 H1). Qed. Lemma BQ_inv_pr_l: forall x y, inc x BQ -> inc y BQ -> BQmult y x = BQ_one -> y = BQinv x. Proof. ir. rwi BQ_mult_comm H1. app BQ_inv_pr_r. Qed. Lemma BQ_inv_opp: forall x, inc x BQ -> BQopp (BQinv x) = BQinv (BQopp x). Proof. ir. nin (equal_or_not x BQ_zero). rw H0. qw. rw BQ_inv_0. qw. cp (BQ_stable_opp H). app BQ_inv_pr_l. app BQ_stable_opp. app BQ_stable_inv. rww BQmult_opp_opp. app BQ_mult_inv_l. app BQ_stable_inv. Qed. Hint Resolve BQ_stable_inv : qprops. Lemma BQps_stable_inv: forall x, inc x BQps -> inc (BQinv x) BQps. Proof. ir. rw inc_BQps_pr. split. qprops. rw BQ_inv_pos. aw. app BQ_Qps. qprops. am. Qed. Lemma BQms_stable_inv: forall x, inc x BQms -> inc (BQinv x) BQms. Proof. ir. wr (BQopp_involutive (sub_BQms_BQ H)). wr BQ_inv_opp. app BQopp_positive1. app BQps_stable_inv. app BQopp_negative1. qprops. Qed. Lemma BQ_inv_sign: forall x, inc x BQ -> BQsign x = BQsign (BQinv x). Proof. ir. cp H. rwi inc_BQ1 H. nin H. rw H. rww BQ_inv_0. nin H. rww BQ_sign_pos. rww BQ_sign_pos. app BQps_stable_inv. rww BQ_sign_neg. rww BQ_sign_neg. app BQms_stable_inv. Qed. Lemma BQ_inv_abs: forall x, inc x BQ -> BQinv (BQabs x) = BQabs (BQinv x). Proof. ir. cp H. rwi inc_BQ1 H. nin H. rw H. rww BQ_inv_0. rw BQ_abs_zero. rww BQ_inv_0. nin H. rww BQ_abs_pos. rww BQ_abs_pos. app sub_BQps_BQp. app BQps_stable_inv. app sub_BQps_BQp. rww BQ_abs_neg. rww BQ_abs_neg. sy. app BQ_inv_opp. app BQms_stable_inv. Qed. Lemma BQ_inv_mult: forall x y, inc x BQ -> inc y BQ -> BQinv (BQmult x y) = BQmult (BQinv x) (BQinv y). Proof. ir. nin (equal_or_not x BQ_zero). rw H1. qw. rw BQ_inv_0. qw. qprops. nin (equal_or_not y BQ_zero). rw H2. qw. rw BQ_inv_0. qw. qprops. sy. cp (BQ_stable_inv x). cp (BQ_stable_inv y). app BQ_inv_pr_r. app BQ_stable_mult. app BQ_stable_mult. rw BQ_mult_permute_2_in_4. rww BQ_mult_inv_r. rww BQ_mult_inv_r. qw. qprops. am. am. am. am. Qed. Lemma BQ_inv_1: BQinv BQ_one = BQ_one. Proof. sy. cp inc1_BQ. app BQ_inv_pr_r. qw. Qed. Lemma BQ_inv_m1: BQinv BQ_mone = BQ_mone. Proof. wr BQ_opp_one. wr BQ_inv_opp. rww BQ_inv_1. qprops. Qed. Lemma BQ_stable_div: forall a b, inc a BQ -> inc b BQ -> inc (BQdiv a b) BQ. Proof. ir. uf BQdiv. app BQ_stable_mult. app BQ_stable_inv. Qed. Lemma BQdiv_mult: forall n m, inc n BQ -> inc m BQ -> n <> BQ_zero -> BQdiv (BQmult n m) n = m. Proof. ir. uf BQdiv. rww (BQ_mult_comm n m). wrr BQ_mult_assoc. rww BQ_mult_inv_r. qw. qprops. Qed. Lemma BQmult_div: forall n m, inc n BQ -> inc m BQ -> n <> BQ_zero -> BQmult n (BQdiv m n) = m. Proof. ir. uf BQdiv. rww (BQ_mult_comm m (BQinv n)). rww BQ_mult_assoc. rww BQ_mult_inv_r. qw. qprops. Qed. Lemma BQmult_div_ea: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> m <> BQ_zero -> n = BQmult m p -> p = BQdiv n m. Proof. ir. rw H3. sy. app BQdiv_mult. Qed. Lemma BQdiv_diag: forall a, inc a BQ -> a <> BQ_zero -> BQdiv a a = BQ_one. Proof. ir. uf BQdiv. rww BQ_mult_inv_r. Qed. Lemma BQ_div_diag_rw: forall a b, inc a BQ -> inc b BQ -> BQdiv a b = BQ_one -> a = b. Proof. ir. cp (f_equal (BQmult b) H1). nin (equal_or_not b BQ_zero). rwi H3 H1. ufi BQdiv H1. rwi BQ_inv_0 H1. qwi H1. elim BQ_one_not_zero. sy; am. am. rwii BQmult_div H2. qwi H2. am. am. Qed. Lemma BQdiv_1_r: forall a, inc a BQ -> BQdiv a BQ_one = a. Proof. ir. uf BQdiv. rw BQ_inv_1. qw. Qed. Lemma BQdiv_1_l: forall a, inc a BQ -> BQdiv BQ_one a = BQinv a. Proof. ir. uf BQdiv. qw. qprops. Qed. Lemma BQdiv_mult_simpl_l: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> p <> BQ_zero -> BQdiv (BQmult p n) (BQmult p m) = BQdiv n m. Proof. ir. uf BQdiv. rw BQ_inv_mult. rw (BQ_mult_comm p n). cp (BQ_stable_inv p). cp (BQ_stable_inv m). rww BQ_mult_assoc. wrr (BQ_mult_assoc H H1 H3). rww BQ_mult_inv_r. qw. app BQ_stable_mult. am. am. Qed. Lemma BQdiv_mult_simpl_r: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> p <> BQ_zero -> BQdiv (BQmult n p) (BQmult m p) = BQdiv n m. Proof. ir. rw (BQ_mult_comm n p). rw (BQ_mult_comm m p). app BQdiv_mult_simpl_l. Qed. Lemma BQdiv_mult_comm: forall n m p, inc n BQ -> inc m BQ ->inc p BQ -> BQdiv (BQmult n m) p = BQmult (BQdiv n p) m. Proof. ir. uf BQdiv. rw (BQ_mult_comm n m). wrr BQ_mult_assoc. rww BQ_mult_comm. qprops. Qed. (* exists unique automorphism z -> z non trivial *) (* exists pos automorphism q -> q non trivial *) (* zed : infinite cyclic group *) (* Q prime field of characteristic zero *) (* char 0 *) (* BQmult_abs *) End RationalNumbers. Export RationalNumbers.