diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NSub.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index de0c2da1b..1df032ea3 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -214,6 +214,17 @@ apply add_sub_eq_nz in EQ; [|order]. rewrite (add_lt_mono_r _ _ n), add_0_l in LT. order. Qed. +Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p. +Proof. + intros. rewrite le_sub_le_add_r. transitivity m. assumption. apply sub_add_le. +Qed. + +Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n. +Proof. + intros. rewrite le_sub_le_add_r. + transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l]. +Qed. + (** Sub and mul *) Theorem mul_pred_r : forall n m, n * (P m) == n * m - n. |