From a79d4d915f64d0eb8d2da4a0ba4d29048b94306b Mon Sep 17 00:00:00 2001
From: thery
Date: Sun, 31 May 2020 16:35:28 +0200
Subject: Extra theorems about subn min and max

---
 mathcomp/ssreflect/ssrnat.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 6837eb1..90b1f1d 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -673,6 +673,13 @@ Proof. by move=> m1 m2 n; rewrite !maxnE subnDr addnAC. Qed.
 Lemma addn_maxr : right_distributive addn maxn.
 Proof. by move=> m n1 n2; rewrite !(addnC m) addn_maxl. Qed.
 
+Lemma subn_maxl : left_distributive subn maxn.
+Proof.
+move=> m n p; apply/eqP.
+rewrite eqn_leq !geq_max !leq_sub2r leq_max ?leqnn ?andbT ?orbT // /maxn.
+by case: (_ < _); rewrite leqnn // orbT.
+Qed.
+
 Lemma min0n : left_zero 0 minn. Proof. by case. Qed.
 Lemma minn0 : right_zero 0 minn. Proof. by []. Qed.
 
@@ -734,6 +741,13 @@ Proof. by move=> m1 m2 n; rewrite !minnE subnDl addnBA ?leq_subr. Qed.
 Lemma addn_minl : left_distributive addn minn.
 Proof. by move=> m1 m2 n; rewrite -!(addnC n) addn_minr. Qed.
 
+Lemma subn_minl : left_distributive subn minn.
+Proof.
+move=> m n p; apply/eqP.
+rewrite eqn_leq !leq_min !leq_sub2r geq_min ?leqnn ?orbT //= /minn.
+by case: (_ < _); rewrite leqnn // orbT.
+Qed.
+
 Lemma minnSS m n : minn m.+1 n.+1 = (minn m n).+1.
 Proof. by rewrite -(addn_minr 1). Qed.
 
-- 
cgit v1.2.3