diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZTimesOrder.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZTimesOrder.v | 67 |
1 files changed, 44 insertions, 23 deletions
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 6fc0078c0..4b4516069 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -200,11 +200,11 @@ Theorem NZtimes_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p Proof. NZord_induct p. intros n m H; false_hyp H NZlt_irrefl. -intros p H1 _ n m H2. apply NZlt_succ_lt in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. -intros p H IH n m H1. apply -> NZlt_le_succ in H. +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_plus_lt n1 m1). -now le_less. do 2 rewrite <- NZtimes_succ_l. now apply -> IH. +now apply NZlt_le_incl. do 2 rewrite <- NZtimes_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. @@ -222,17 +222,17 @@ Qed. Theorem NZtimes_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. le_less. now apply -> NZtimes_lt_mono_pos_l. -le_equal; now rewrite H2. -le_equal; rewrite <- H1; now do 2 rewrite NZtimes_0_l. +le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_pos_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZtimes_0_l. Qed. Theorem NZtimes_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. le_less. now apply -> NZtimes_lt_mono_neg_l. -le_equal; now rewrite H2. -le_equal; rewrite H1; now do 2 rewrite NZtimes_0_l. +le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_neg_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZtimes_0_l. Qed. Theorem NZtimes_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. @@ -272,7 +272,7 @@ Qed. Theorem NZtimes_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 NZle_lt_or_eq. +intros n m p H; do 2 rewrite NZlt_eq_cases. rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |]. now rewrite -> (NZtimes_cancel_l n m p); [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. @@ -286,7 +286,7 @@ Qed. Theorem NZtimes_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 NZle_lt_or_eq. +intros n m p H; do 2 rewrite NZlt_eq_cases. rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |]. rewrite -> (NZtimes_cancel_l m n p); [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. @@ -304,7 +304,7 @@ Theorem NZtimes_lt_mono : Proof. intros n m p q H1 H2 H3 H4. apply NZle_lt_trans with (m * p). -apply NZtimes_le_mono_nonneg_r; [assumption | now le_less]. +apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. apply -> NZtimes_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. Qed. @@ -316,10 +316,10 @@ Theorem NZtimes_le_mono : Proof. intros n m p q H1 H2 H3 H4. le_elim H2; le_elim H4. -le_less; now apply NZtimes_lt_mono. -rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now le_less]. -rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now le_less]. -rewrite H2; rewrite H4; now le_equal. +apply NZlt_le_incl; now apply NZtimes_lt_mono. +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. Qed. Theorem NZtimes_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. @@ -368,25 +368,46 @@ Proof. intros; rewrite NZtimes_comm; now apply NZtimes_nonneg_nonpos. Qed. -Theorem NZtimes_eq_0 : forall n m : NZ, n * m == 0 -> n == 0 \/ m == 0. +Theorem NZlt_1_times_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. Proof. -intros n m H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1. +rewrite NZtimes_1_l in H1. now apply NZlt_1_l with m. +assumption. +Qed. + +Theorem NZeq_times_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 NZtimes_neg_neg |]. elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_neg_pos |]. elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_pos_neg |]. elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_pos_pos |]. +intros [H | H]. now rewrite H, NZtimes_0_l. now rewrite H, NZtimes_0_r. Qed. -Theorem NZtimes_neq_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Theorem NZneq_times_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof. intros n m; split; intro H. -intro H1; apply NZtimes_eq_0 in H1. tauto. +intro H1; apply -> NZeq_times_0 in H1. tauto. split; intro H1; rewrite H1 in H; (rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H. Qed. +Theorem NZeq_times_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. +Proof. +intros n m H1 H2. apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1]. +assumption. false_hyp H1 H2. +Qed. + +Theorem NZeq_times_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. +Proof. +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). Proof. intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. @@ -420,12 +441,12 @@ Qed. Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. Proof. -intros n m H. apply -> NZlt_le_succ in H. +intros n m H. apply <- NZle_succ_l in H. apply -> (NZtimes_le_mono_pos_l (S n) m (1 + 1)) in H. repeat rewrite NZtimes_plus_distr_r in *; repeat rewrite NZtimes_1_l in *. repeat rewrite NZplus_succ_r in *. repeat rewrite NZplus_succ_l in *. rewrite NZplus_0_l. -now apply <- NZlt_le_succ. -apply NZplus_pos_pos; now apply NZlt_succ_r. +now apply -> NZle_succ_l. +apply NZplus_pos_pos; now apply NZlt_succ_diag_r. Qed. End NZTimesOrderPropFunct. |