From ebb3fe944b6bd1cd363e3348465d7ea2fd85c62c Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 3 Jun 2008 00:04:16 +0000 Subject: In abstract parts of theories/Numbers, plus/times becomes add/mul, for increased consistency with bignums parts (commit part II: names of files + additional translation minus --> sub) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/NatInt/NZAdd.v | 91 ++++++++++ theories/Numbers/NatInt/NZAddOrder.v | 166 ++++++++++++++++++ theories/Numbers/NatInt/NZAxioms.v | 14 +- theories/Numbers/NatInt/NZMul.v | 80 +++++++++ theories/Numbers/NatInt/NZMulOrder.v | 310 +++++++++++++++++++++++++++++++++ theories/Numbers/NatInt/NZOrder.v | 4 +- theories/Numbers/NatInt/NZPlus.v | 91 ---------- theories/Numbers/NatInt/NZPlusOrder.v | 166 ------------------ theories/Numbers/NatInt/NZTimes.v | 80 --------- theories/Numbers/NatInt/NZTimesOrder.v | 310 --------------------------------- 10 files changed, 656 insertions(+), 656 deletions(-) create mode 100644 theories/Numbers/NatInt/NZAdd.v create mode 100644 theories/Numbers/NatInt/NZAddOrder.v create mode 100644 theories/Numbers/NatInt/NZMul.v create mode 100644 theories/Numbers/NatInt/NZMulOrder.v delete mode 100644 theories/Numbers/NatInt/NZPlus.v delete mode 100644 theories/Numbers/NatInt/NZPlusOrder.v delete mode 100644 theories/Numbers/NatInt/NZTimes.v delete mode 100644 theories/Numbers/NatInt/NZTimesOrder.v (limited to 'theories/Numbers/NatInt') diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v new file mode 100644 index 0000000000..9c852bf908 --- /dev/null +++ b/theories/Numbers/NatInt/NZAdd.v @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* n == m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. +Proof. +intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). +apply NZadd_cancel_l. +Qed. + +Theorem NZsub_1_r : forall n : NZ, n - 1 == P n. +Proof. +intro n; rewrite NZsub_succ_r; now rewrite NZsub_0_r. +Qed. + +End NZAddPropFunct. + diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v new file mode 100644 index 0000000000..d1caa83eeb --- /dev/null +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -0,0 +1,166 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* p + n < p + m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_lt_mono. +Qed. + +Theorem NZadd_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p. +Proof. +intros n m p. +rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_lt_mono_l. +Qed. + +Theorem NZadd_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZlt_trans with (m + p); +[now apply -> NZadd_lt_mono_r | now apply -> NZadd_lt_mono_l]. +Qed. + +Theorem NZadd_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_le_mono. +Qed. + +Theorem NZadd_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p. +Proof. +intros n m p. +rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_le_mono_l. +Qed. + +Theorem NZadd_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q. +Proof. +intros n m p q H1 H2. +apply NZle_trans with (m + p); +[now apply -> NZadd_le_mono_r | now apply -> NZadd_le_mono_l]. +Qed. + +Theorem NZadd_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZlt_le_trans with (m + p); +[now apply -> NZadd_lt_mono_r | now apply -> NZadd_le_mono_l]. +Qed. + +Theorem NZadd_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZle_lt_trans with (m + p); +[now apply -> NZadd_le_mono_r | now apply -> NZadd_lt_mono_l]. +Qed. + +Theorem NZadd_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_mono. +Qed. + +Theorem NZadd_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_le_mono. +Qed. + +Theorem NZadd_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_lt_mono. +Qed. + +Theorem NZadd_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_mono. +Qed. + +Theorem NZlt_add_pos_l : forall n m : NZ, 0 < n -> m < n + m. +Proof. +intros n m H. apply -> (NZadd_lt_mono_r 0 n m) in H. +now rewrite NZadd_0_l in H. +Qed. + +Theorem NZlt_add_pos_r : forall n m : NZ, 0 < n -> m < m + n. +Proof. +intros; rewrite NZadd_comm; now apply NZlt_add_pos_l. +Qed. + +Theorem NZle_lt_add_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. +pose proof (NZadd_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. +false_hyp H3 H2. +Qed. + +Theorem NZlt_le_add_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. +pose proof (NZadd_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZle_le_add_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |]. +pose proof (NZadd_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZadd_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. +Proof. +intros n m p q H; +destruct (NZle_gt_cases p n) as [H1 | H1]. +destruct (NZle_gt_cases q m) as [H2 | H2]. +pose proof (NZadd_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3. +false_hyp H H3. +now right. now left. +Qed. + +Theorem NZadd_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. +Proof. +intros n m p q H. +destruct (NZle_gt_cases n p) as [H1 | H1]. now left. +destruct (NZle_gt_cases m q) as [H2 | H2]. now right. +assert (H3 : p + q < n + m) by now apply NZadd_lt_mono. +apply -> NZle_ngt in H. false_hyp H3 H. +Qed. + +Theorem NZadd_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. +Proof. +intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Proof. +intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. +Proof. +intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. +Proof. +intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. +Qed. + +End NZAddOrderPropFunct. + diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 516cf5b42b..1ef7809866 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -20,11 +20,11 @@ Parameter Inline NZ0 : NZ. Parameter Inline NZsucc : NZ -> NZ. Parameter Inline NZpred : NZ -> NZ. Parameter Inline NZadd : NZ -> NZ -> NZ. -Parameter Inline NZminus : NZ -> NZ -> NZ. +Parameter Inline NZsub : NZ -> NZ -> NZ. Parameter Inline NZmul : NZ -> NZ -> NZ. -(* Unary minus (opp) is not defined on natural numbers, so we have it for -integers only *) +(* Unary subtraction (opp) is not defined on natural numbers, so we have + it for integers only *) Axiom NZeq_equiv : equiv NZ NZeq. Add Relation NZ NZeq @@ -36,7 +36,7 @@ as NZeq_rel. Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. Delimit Scope NatIntScope with NatInt. @@ -48,7 +48,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation "1" := (S 0) : NatIntScope. Notation "x + y" := (NZadd x y) : NatIntScope. -Notation "x - y" := (NZminus x y) : NatIntScope. +Notation "x - y" := (NZsub x y) : NatIntScope. Notation "x * y" := (NZmul x y) : NatIntScope. Axiom NZpred_succ : forall n : NZ, P (S n) == n. @@ -60,8 +60,8 @@ Axiom NZinduction : Axiom NZadd_0_l : forall n : NZ, 0 + n == n. Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m). -Axiom NZminus_0_r : forall n : NZ, n - 0 == n. -Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Axiom NZsub_0_r : forall n : NZ, n - 0 == n. +Axiom NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). Axiom NZmul_0_l : forall n : NZ, 0 * n == 0. Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v new file mode 100644 index 0000000000..7d9b1aabd3 --- /dev/null +++ b/theories/Numbers/NatInt/NZMul.v @@ -0,0 +1,80 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (p * n < p * m <-> q * n + m < q * m + n). +Proof. +intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l. +rewrite <- (NZadd_assoc (p * n) n m). +rewrite <- (NZadd_assoc (p * m) m n). +rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r. +Qed. + +Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m). +Proof. +NZord_induct p. +intros n m H; false_hyp H NZlt_irrefl. +intros p H IH n m H1. do 2 rewrite NZmul_succ_l. +le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m). +intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption]. +split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. +apply <- NZle_ngt in H3. le_elim H3. +apply NZlt_asymm in H2. apply H2. now apply LR. +rewrite H3 in H2; false_hyp H2 NZlt_irrefl. +rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. +intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1. +Qed. + +Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p). +Proof. +intros p n m. +rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l. +Qed. + +Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n). +Proof. +NZord_induct p. +intros n m H; false_hyp H NZlt_irrefl. +intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. +intros p H IH n m H1. apply <- NZle_succ_l in H. +le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n). +intros n1 m1 H2. apply (NZle_lt_add_lt n1 m1). +now apply NZlt_le_incl. do 2 rewrite <- NZmul_succ_l. now apply -> IH. +split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. +apply <- NZle_ngt in H3. le_elim H3. +apply NZlt_asymm in H2. apply H2. now apply LR. +rewrite H3 in H2; false_hyp H2 NZlt_irrefl. +rewrite (NZmul_lt_pred p (S p)) by reflexivity. +rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. +Qed. + +Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p). +Proof. +intros p n m. +rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l. +Qed. + +Theorem NZmul_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m. +Proof. +intros n m p H1 H2. le_elim H1. +le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l. +Qed. + +Theorem NZmul_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n. +Proof. +intros n m p H1 H2. le_elim H1. +le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l. +Qed. + +Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. +Proof. +intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +now apply NZmul_le_mono_nonneg_l. +Qed. + +Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p. +Proof. +intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +now apply NZmul_le_mono_nonpos_l. +Qed. + +Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m). +Proof. +intros n m p H; split; intro H1. +destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]]. +apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. +assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |]. +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |]. +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +false_hyp H2 H. +apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. +assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l). +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l). +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +now rewrite H1. +Qed. + +Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m). +Proof. +intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l. +Qed. + +Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1). +Proof. +intros n m H. +stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r. +Qed. + +Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1). +Proof. +intros n m; rewrite NZmul_comm; apply NZmul_id_l. +Qed. + +Theorem NZmul_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m). +Proof. +intros n m p H; do 2 rewrite NZlt_eq_cases. +rewrite (NZmul_lt_mono_pos_l p n m) by assumption. +now rewrite -> (NZmul_cancel_l n m p) by +(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). +Qed. + +Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p). +Proof. +intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +apply NZmul_le_mono_pos_l. +Qed. + +Theorem NZmul_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n). +Proof. +intros n m p H; do 2 rewrite NZlt_eq_cases. +rewrite (NZmul_lt_mono_neg_l p n m); [| assumption]. +rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). +now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro). +Qed. + +Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p). +Proof. +intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +apply NZmul_le_mono_neg_l. +Qed. + +Theorem NZmul_lt_mono_nonneg : + forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. +Proof. +intros n m p q H1 H2 H3 H4. +apply NZle_lt_trans with (m * p). +apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. +apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. +Qed. + +(* There are still many variants of the theorem above. One can assume 0 < n +or 0 < p or n <= m or p <= q. *) + +Theorem NZmul_le_mono_nonneg : + forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. +Proof. +intros n m p q H1 H2 H3 H4. +le_elim H2; le_elim H4. +apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg. +rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. +rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl]. +rewrite H2; rewrite H4; now apply NZeq_le_incl. +Qed. + +Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r. +Qed. + +Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. +Qed. + +Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. +Qed. + +Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0. +Proof. +intros; rewrite NZmul_comm; now apply NZmul_pos_neg. +Qed. + +Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. +rewrite NZmul_1_l in H1. now apply NZlt_1_l with m. +assumption. +Qed. + +Theorem NZeq_mul_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0. +Proof. +intros n m; split. +intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; +try (now right); try (now left). +elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |]. +elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |]. +elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |]. +elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |]. +intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r. +Qed. + +Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof. +intros n m; split; intro H. +intro H1; apply -> NZeq_mul_0 in H1. tauto. +split; intro H1; rewrite H1 in H; +(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H. +Qed. + +Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0. +Proof. +intro n; rewrite NZeq_mul_0; tauto. +Qed. + +Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. +Proof. +intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. +assumption. false_hyp H1 H2. +Qed. + +Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. +Proof. +intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. +false_hyp H1 H2. assumption. +Qed. + +Theorem NZlt_0_mul : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). +Proof. +intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. +destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +[| rewrite H1 in H; rewrite NZmul_0_l in H; false_hyp H NZlt_irrefl |]; +(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]); +try (left; now split); try (right; now split). +assert (H3 : n * m < 0) by now apply NZmul_neg_pos. +elimtype False; now apply (NZlt_asymm (n * m) 0). +assert (H3 : n * m < 0) by now apply NZmul_pos_neg. +elimtype False; now apply (NZlt_asymm (n * m) 0). +now apply NZmul_pos_pos. now apply NZmul_neg_neg. +Qed. + +Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m. +Proof. +intros n m H1 H2. now apply NZmul_lt_mono_nonneg. +Qed. + +Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m. +Proof. +intros n m H1 H2. now apply NZmul_le_mono_nonneg. +Qed. + +(* The converse theorems require nonnegativity (or nonpositivity) of the +other variable *) + +Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +now apply NZlt_le_trans with 0. +destruct (NZlt_ge_cases n m). +assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg. +apply -> NZle_ngt in F. false_hyp H2 F. +Qed. + +Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +apply NZlt_le_incl; now apply NZlt_le_trans with 0. +destruct (NZle_gt_cases n m). +assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg. +apply -> NZlt_nge in F. false_hyp H2 F. +Qed. + +Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof. +intros n m H. apply <- NZle_succ_l in H. +apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H. +repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *. +repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l. +now apply -> NZle_succ_l. +apply NZadd_pos_pos; now apply NZlt_succ_diag_r. +Qed. + +End NZMulOrderPropFunct. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index f76fa94808..d8eaeb99c2 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -11,11 +11,11 @@ (*i $Id$ i*) Require Import NZAxioms. -Require Import NZTimes. +Require Import NZMul. Require Import Decidable. Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). -Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod. +Module Export NZMulPropMod := NZMulPropFunct NZAxiomsMod. Open Local Scope NatIntScope. Ltac le_elim H := rewrite NZlt_eq_cases in H; destruct H as [H | H]. diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v deleted file mode 100644 index 6fb72ed4a9..0000000000 --- a/theories/Numbers/NatInt/NZPlus.v +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* n == m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZadd_0_l. -intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. -Qed. - -Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. -Proof. -intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). -apply NZadd_cancel_l. -Qed. - -Theorem NZminus_1_r : forall n : NZ, n - 1 == P n. -Proof. -intro n; rewrite NZminus_succ_r; now rewrite NZminus_0_r. -Qed. - -End NZPlusPropFunct. - diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v deleted file mode 100644 index 00d178c0d9..0000000000 --- a/theories/Numbers/NatInt/NZPlusOrder.v +++ /dev/null @@ -1,166 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* p + n < p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZadd_0_l. -intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_lt_mono. -Qed. - -Theorem NZadd_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p. -Proof. -intros n m p. -rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_lt_mono_l. -Qed. - -Theorem NZadd_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_trans with (m + p); -[now apply -> NZadd_lt_mono_r | now apply -> NZadd_lt_mono_l]. -Qed. - -Theorem NZadd_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZadd_0_l. -intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_le_mono. -Qed. - -Theorem NZadd_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p. -Proof. -intros n m p. -rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_le_mono_l. -Qed. - -Theorem NZadd_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q. -Proof. -intros n m p q H1 H2. -apply NZle_trans with (m + p); -[now apply -> NZadd_le_mono_r | now apply -> NZadd_le_mono_l]. -Qed. - -Theorem NZadd_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_le_trans with (m + p); -[now apply -> NZadd_lt_mono_r | now apply -> NZadd_le_mono_l]. -Qed. - -Theorem NZadd_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZle_lt_trans with (m + p); -[now apply -> NZadd_le_mono_r | now apply -> NZadd_lt_mono_l]. -Qed. - -Theorem NZadd_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_mono. -Qed. - -Theorem NZadd_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_le_mono. -Qed. - -Theorem NZadd_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_lt_mono. -Qed. - -Theorem NZadd_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_mono. -Qed. - -Theorem NZlt_add_pos_l : forall n m : NZ, 0 < n -> m < n + m. -Proof. -intros n m H. apply -> (NZadd_lt_mono_r 0 n m) in H. -now rewrite NZadd_0_l in H. -Qed. - -Theorem NZlt_add_pos_r : forall n m : NZ, 0 < n -> m < m + n. -Proof. -intros; rewrite NZadd_comm; now apply NZlt_add_pos_l. -Qed. - -Theorem NZle_lt_add_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. -Proof. -intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. -pose proof (NZadd_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. -false_hyp H3 H2. -Qed. - -Theorem NZlt_le_add_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q. -Proof. -intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. -pose proof (NZadd_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. -false_hyp H2 H3. -Qed. - -Theorem NZle_le_add_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. -Proof. -intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |]. -pose proof (NZadd_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. -false_hyp H2 H3. -Qed. - -Theorem NZadd_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. -Proof. -intros n m p q H; -destruct (NZle_gt_cases p n) as [H1 | H1]. -destruct (NZle_gt_cases q m) as [H2 | H2]. -pose proof (NZadd_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3. -false_hyp H H3. -now right. now left. -Qed. - -Theorem NZadd_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. -Proof. -intros n m p q H. -destruct (NZle_gt_cases n p) as [H1 | H1]. now left. -destruct (NZle_gt_cases m q) as [H2 | H2]. now right. -assert (H3 : p + q < n + m) by now apply NZadd_lt_mono. -apply -> NZle_ngt in H. false_hyp H3 H. -Qed. - -Theorem NZadd_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. -Proof. -intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. -Qed. - -Theorem NZadd_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. -Proof. -intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. -Qed. - -Theorem NZadd_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. -Proof. -intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. -Qed. - -Theorem NZadd_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. -Proof. -intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. -Qed. - -End NZPlusOrderPropFunct. - diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v deleted file mode 100644 index 9f93e0a1bf..0000000000 --- a/theories/Numbers/NatInt/NZTimes.v +++ /dev/null @@ -1,80 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (p * n < p * m <-> q * n + m < q * m + n). -Proof. -intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l. -rewrite <- (NZadd_assoc (p * n) n m). -rewrite <- (NZadd_assoc (p * m) m n). -rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r. -Qed. - -Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m). -Proof. -NZord_induct p. -intros n m H; false_hyp H NZlt_irrefl. -intros p H IH n m H1. do 2 rewrite NZmul_succ_l. -le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m). -intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption]. -split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. -apply <- NZle_ngt in H3. le_elim H3. -apply NZlt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 NZlt_irrefl. -rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. -intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1. -Qed. - -Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p). -Proof. -intros p n m. -rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l. -Qed. - -Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n). -Proof. -NZord_induct p. -intros n m H; false_hyp H NZlt_irrefl. -intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. -intros p H IH n m H1. apply <- NZle_succ_l in H. -le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n). -intros n1 m1 H2. apply (NZle_lt_add_lt n1 m1). -now apply NZlt_le_incl. do 2 rewrite <- NZmul_succ_l. now apply -> IH. -split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. -apply <- NZle_ngt in H3. le_elim H3. -apply NZlt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 NZlt_irrefl. -rewrite (NZmul_lt_pred p (S p)) by reflexivity. -rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. -Qed. - -Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p). -Proof. -intros p n m. -rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l. -Qed. - -Theorem NZmul_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m. -Proof. -intros n m p H1 H2. le_elim H1. -le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l. -apply NZeq_le_incl; now rewrite H2. -apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l. -Qed. - -Theorem NZmul_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n. -Proof. -intros n m p H1 H2. le_elim H1. -le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l. -apply NZeq_le_incl; now rewrite H2. -apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l. -Qed. - -Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. -Proof. -intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -now apply NZmul_le_mono_nonneg_l. -Qed. - -Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p. -Proof. -intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -now apply NZmul_le_mono_nonpos_l. -Qed. - -Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m). -Proof. -intros n m p H; split; intro H1. -destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]]. -apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -false_hyp H2 H. -apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -now rewrite H1. -Qed. - -Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m). -Proof. -intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l. -Qed. - -Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1). -Proof. -intros n m H. -stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r. -Qed. - -Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1). -Proof. -intros n m; rewrite NZmul_comm; apply NZmul_id_l. -Qed. - -Theorem NZmul_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m). -Proof. -intros n m p H; do 2 rewrite NZlt_eq_cases. -rewrite (NZmul_lt_mono_pos_l p n m) by assumption. -now rewrite -> (NZmul_cancel_l n m p) by -(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). -Qed. - -Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p). -Proof. -intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -apply NZmul_le_mono_pos_l. -Qed. - -Theorem NZmul_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n). -Proof. -intros n m p H; do 2 rewrite NZlt_eq_cases. -rewrite (NZmul_lt_mono_neg_l p n m); [| assumption]. -rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). -now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro). -Qed. - -Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p). -Proof. -intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -apply NZmul_le_mono_neg_l. -Qed. - -Theorem NZmul_lt_mono_nonneg : - forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. -Proof. -intros n m p q H1 H2 H3 H4. -apply NZle_lt_trans with (m * p). -apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. -apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. -Qed. - -(* There are still many variants of the theorem above. One can assume 0 < n -or 0 < p or n <= m or p <= q. *) - -Theorem NZmul_le_mono_nonneg : - forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. -Proof. -intros n m p q H1 H2 H3 H4. -le_elim H2; le_elim H4. -apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg. -rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. -rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl]. -rewrite H2; rewrite H4; now apply NZeq_le_incl. -Qed. - -Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. -Proof. -intros n m H1 H2. -rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r. -Qed. - -Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m. -Proof. -intros n m H1 H2. -rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. -Qed. - -Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0. -Proof. -intros n m H1 H2. -rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. -Qed. - -Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0. -Proof. -intros; rewrite NZmul_comm; now apply NZmul_pos_neg. -Qed. - -Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. -Proof. -intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. -rewrite NZmul_1_l in H1. now apply NZlt_1_l with m. -assumption. -Qed. - -Theorem NZeq_mul_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0. -Proof. -intros n m; split. -intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; -destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; -try (now right); try (now left). -elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |]. -elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |]. -elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |]. -elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |]. -intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r. -Qed. - -Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof. -intros n m; split; intro H. -intro H1; apply -> NZeq_mul_0 in H1. tauto. -split; intro H1; rewrite H1 in H; -(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H. -Qed. - -Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0. -Proof. -intro n; rewrite NZeq_mul_0; tauto. -Qed. - -Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. -Proof. -intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. -assumption. false_hyp H1 H2. -Qed. - -Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. -Proof. -intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. -false_hyp H1 H2. assumption. -Qed. - -Theorem NZlt_0_mul : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). -Proof. -intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. -destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; -[| rewrite H1 in H; rewrite NZmul_0_l in H; false_hyp H NZlt_irrefl |]; -(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; -[| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]); -try (left; now split); try (right; now split). -assert (H3 : n * m < 0) by now apply NZmul_neg_pos. -elimtype False; now apply (NZlt_asymm (n * m) 0). -assert (H3 : n * m < 0) by now apply NZmul_pos_neg. -elimtype False; now apply (NZlt_asymm (n * m) 0). -now apply NZmul_pos_pos. now apply NZmul_neg_neg. -Qed. - -Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m. -Proof. -intros n m H1 H2. now apply NZmul_lt_mono_nonneg. -Qed. - -Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m. -Proof. -intros n m H1 H2. now apply NZmul_le_mono_nonneg. -Qed. - -(* The converse theorems require nonnegativity (or nonpositivity) of the -other variable *) - -Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m. -Proof. -intros n m H1 H2. destruct (NZlt_ge_cases n 0). -now apply NZlt_le_trans with 0. -destruct (NZlt_ge_cases n m). -assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg. -apply -> NZle_ngt in F. false_hyp H2 F. -Qed. - -Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m. -Proof. -intros n m H1 H2. destruct (NZlt_ge_cases n 0). -apply NZlt_le_incl; now apply NZlt_le_trans with 0. -destruct (NZle_gt_cases n m). -assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg. -apply -> NZlt_nge in F. false_hyp H2 F. -Qed. - -Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. -Proof. -intros n m H. apply <- NZle_succ_l in H. -apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H. -repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *. -repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l. -now apply -> NZle_succ_l. -apply NZadd_pos_pos; now apply NZlt_succ_diag_r. -Qed. - -End NZTimesOrderPropFunct. -- cgit v1.2.3