diff options
Diffstat (limited to 'theories/ZArith/Zorder.v')
| -rw-r--r-- | theories/ZArith/Zorder.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index f907b788d..ea7b42147 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -967,5 +967,17 @@ intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l; rewrite Zplus_comm; exact H. Qed. +Lemma Zle_0_minus_le : forall n m:Z, 0 <= n - m -> m <= n. +Proof. +intros n m H; apply Zplus_le_reg_l with (p := - m); rewrite Zplus_opp_l; + rewrite Zplus_comm; exact H. +Qed. + +Lemma Zle_minus_le_0 : forall n m:Z, m <= n -> 0 <= n - m. +Proof. +intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m); +rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. +Qed. + (* For compatibility *) Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing). |