Added theorems; created NZPlusOrder from NTimesOrder.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10325 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 34 insertions, 191 deletions

diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 4b4516069e..aac823dc40 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -11,161 +11,12 @@
 (*i i*)
 
 Require Import NZAxioms.
-Require Import NZOrder.
+Require Import NZPlusOrder.
 
 Module NZTimesOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
-Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod.
+Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZOrdAxiomsMod.
 Open Local Scope NatIntScope.
 
-(** Addition and order *)
-
-Theorem NZplus_lt_mono_l : forall n m p : NZ, n < m <-> p + n < p + m.
-Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono.
-Qed.
-
-Theorem NZplus_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p.
-Proof.
-intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l.
-Qed.
-
-Theorem NZplus_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 -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l].
-Qed.
-
-Theorem NZplus_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 NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono.
-Qed.
-
-Theorem NZplus_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p.
-Proof.
-intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l.
-Qed.
-
-Theorem NZplus_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 -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l].
-Qed.
-
-Theorem NZplus_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 -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l].
-Qed.
-
-Theorem NZplus_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 -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
-Qed.
-
-Theorem NZplus_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m.
-Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_mono.
-Qed.
-
-Theorem NZplus_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m.
-Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_le_mono.
-Qed.
-
-Theorem NZplus_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m.
-Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_lt_mono.
-Qed.
-
-Theorem NZplus_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m.
-Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_mono.
-Qed.
-
-Theorem NZlt_plus_pos_l : forall n m : NZ, 0 < n -> m < n + m.
-Proof.
-intros n m H. apply -> (NZplus_lt_mono_r 0 n m) in H.
-now rewrite NZplus_0_l in H.
-Qed.
-
-Theorem NZlt_plus_pos_r : forall n m : NZ, 0 < n -> m < m + n.
-Proof.
-intros; rewrite NZplus_comm; now apply NZlt_plus_pos_l.
-Qed.
-
-Theorem NZle_lt_plus_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 (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2.
-false_hyp H3 H2.
-Qed.
-
-Theorem NZlt_le_plus_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 (NZplus_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
-false_hyp H2 H3.
-Qed.
-
-Theorem NZle_le_plus_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 (NZplus_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
-false_hyp H2 H3.
-Qed.
-
-Theorem NZplus_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 (NZplus_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 NZplus_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 NZplus_lt_mono.
-apply -> NZle_ngt in H. false_hyp H3 H.
-Qed.
-
-Theorem NZplus_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0.
-Proof.
-intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l.
-Qed.
-
-Theorem NZplus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
-Proof.
-intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l.
-Qed.
-
-Theorem NZplus_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0.
-Proof.
-intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l.
-Qed.
-
-Theorem NZplus_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m.
-Proof.
-intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l.
-Qed.
-
-(** Multiplication and order *)
-
 Theorem NZtimes_lt_pred :
   forall p q n m : NZ, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
 Proof.
@@ -299,7 +150,7 @@ intros n m p. rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
 apply NZtimes_le_mono_neg_l.
 Qed.
 
-Theorem NZtimes_lt_mono :
+Theorem NZtimes_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.
@@ -311,12 +162,12 @@ 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 NZtimes_le_mono :
+Theorem NZtimes_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 NZtimes_lt_mono.
+apply NZlt_le_incl; now apply NZtimes_lt_mono_nonneg.
 rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
 rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl].
 rewrite H2; rewrite H4; now apply NZeq_le_incl.
@@ -328,46 +179,23 @@ intros n m H1 H2.
 rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_pos_r.
 Qed.
 
-Theorem NZtimes_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n * m.
-Proof.
-intros n m H1 H2.
-rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonneg_r.
-Qed.
-
 Theorem NZtimes_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m.
 Proof.
 intros n m H1 H2.
 rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r.
 Qed.
 
-Theorem NZtimes_nonpos_nonpos : forall n m : NZ, n <= 0 -> m <= 0 -> 0 <= n * m.
-Proof.
-intros n m H1 H2.
-rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonpos_r.
-Qed.
-
 Theorem NZtimes_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0.
 Proof.
 intros n m H1 H2.
 rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r.
 Qed.
 
-Theorem NZtimes_nonneg_nonpos : forall n m : NZ, 0 <= n -> m <= 0 -> n * m <= 0.
-Proof.
-intros n m H1 H2.
-rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonpos_r.
-Qed.
-
 Theorem NZtimes_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0.
 Proof.
 intros; rewrite NZtimes_comm; now apply NZtimes_pos_neg.
 Qed.
 
-Theorem NZtimes_nonpos_nonneg : forall n m : NZ, n <= 0 -> 0 <= m -> n * m <= 0.
-Proof.
-intros; rewrite NZtimes_comm; now apply NZtimes_nonneg_nonpos.
-Qed.
-
 Theorem NZlt_1_times_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m.
 Proof.
 intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1.
@@ -408,7 +236,7 @@ intros n m H1 H2; apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1].
 false_hyp H1 H2. assumption.
 Qed.
 
-Theorem NZtimes_pos : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
+Theorem NZlt_0_times : 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]];
@@ -423,20 +251,35 @@ elimtype False; now apply (NZlt_asymm (n * m) 0).
 now apply NZtimes_pos_pos. now apply NZtimes_neg_neg.
 Qed.
 
-Theorem NZtimes_neg :
-  forall n m : NZ, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0).
+Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m.
 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 NZtimes_0_l in H; false_hyp H NZlt_irrefl |];
-(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
-[| rewrite H2 in H; rewrite NZtimes_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 NZtimes_neg_neg.
-elimtype False; now apply (NZlt_asymm (n * m) 0).
-assert (H3 : n * m > 0) by now apply NZtimes_pos_pos.
-elimtype False; now apply (NZlt_asymm (n * m) 0).
-now apply NZtimes_neg_pos. now apply NZtimes_pos_neg.
+intros n m H1 H2. now apply NZtimes_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 NZtimes_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 NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.