From 485151f9ee054b0a0f390d4eff6a2bb2958ed8c2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 23 Jun 2011 16:35:22 +0000
Subject: Some more cleanup of Zorder

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14234 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/NatInt/NZMulOrder.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'theories/Numbers/NatInt')

diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 30a475aeab..97306f9340 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -196,6 +196,30 @@ Proof.
 intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order.
 Qed.
 
+Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m).
+Proof.
+intros n m Hn. rewrite <- (mul_0_r n) at 1.
+ symmetry. now apply mul_lt_mono_pos_l.
+Qed.
+
+Theorem mul_pos_cancel_r : forall n m, 0 < m -> (0 < n*m <-> 0 < n).
+Proof.
+intros n m Hn. rewrite <- (mul_0_l m) at 1.
+ symmetry. now apply mul_lt_mono_pos_r.
+Qed.
+
+Theorem mul_nonneg_cancel_l : forall n m, 0 < n -> (0 <= n*m <-> 0 <= m).
+Proof.
+intros n m Hn. rewrite <- (mul_0_r n) at 1.
+ symmetry. now apply mul_le_mono_pos_l.
+Qed.
+
+Theorem mul_nonneg_cancel_r : forall n m, 0 < m -> (0 <= n*m <-> 0 <= n).
+Proof.
+intros n m Hn. rewrite <- (mul_0_l m) at 1.
+ symmetry. now apply mul_le_mono_pos_r.
+Qed.
+
 Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m.
 Proof.
 intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1.
-- 
cgit v1.2.3