From c35a5da4a400199a1cb48a9e7416e1724a661ce5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 19 Apr 2022 16:17:39 +0200
Subject: [PATCH] fixup! Prepare subdnD for MathComp PR
---
util/nat.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/util/nat.v b/util/nat.v
index 7fa4adfc2..7bedb25bd 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -6,9 +6,9 @@ Require Export prosa.util.tactics.
(** Additional lemmas about natural numbers. *)
Section NatLemmas.
- (** First, we show that, given [m1 >= m2] and [n1 >= n2], an
- expression [(m1 + n1) - (m2 + n2)] can be transformed into
- expression [(m1 - m2) + (n1 - n2)]. *)
+ (** First, we show that, given [m >= p] and [n >= q], an
+ expression [(m + n) - (p + q)] can be transformed into
+ expression [(m - p) + (n - q)]. *)
Lemma subnACA m n p q : p <= m -> q <= n ->
(m + n) - (p + q) = (m - p) + (n - q).
Proof. by move=> plem qlen; rewrite subnDA addnBAC// addnBA// subnAC. Qed.
--
GitLab