Big Data.(Nat/Integer).Properties wishlist

[mechvel]

• Add ⊔-mono-≤ and friends
• Make notations uniform for ≤-<-trans vs. <-transʳ
• >⇒≢ : ∀ {m n} → m > n → m ≢ n
• m+suc[n]≡suc[m]+n : ∀ m n → m + suc n ≡ suc m + n (already exists: +-suc)
• n≢1+n : ∀ {n} → n ≢ suc n (already exists: 1+n≢n)
• 1<2+n : ∀ n → 1 < 2 + n (direct corollary of m<m+n)
• <1⇒≡0 : ∀ {n} → n < 1 → n ≡ 0
• n≤1⇒n≡0∨n≡1 : ∀ {n} → n ≤ 1 → n ≡ 0 ⊎ n ≡ 1
• m<n⇒0<n : ∀ {m n} → m < n → 0 < n
• pred-n≤n : ∀ {n} → pred n ≤ n
• m≤n*m : ∀ m {n} → 0 < n → m ≤ n * m
• m<n⇒n∸m>0 : {m n : ℕ} → m < n → n ∸ m > 0 (already exists: m<n⇒0<n∸m)
• m*[1+n] : ∀ m n → m * (suc n) ≡ m + m * n (already exists: *-suc)
• upTo-n≤n : ∀ n → All (_≤ n) (upTo n) (stronger: all-upTo : All (_< n) (upTo n))
• length-upFrom : ∀ n c → length (upFrom n c) ≡ suc c
• length-from-to : ∀ m n → length (from m to n) ≡ suc (n ∸ m)

[mechvel]

Maybe join it with wishes for Nat.Properties ?
("Big wish list for Data.Nat(Integer).Properties").
For example, I had several wishes for Nat.Properties:
I am not sure, may be some of them do fit.

>⇒≢ : ∀ {m n} → m > n → m ≢ n                                                     
m+suc[n]≡suc[m]+n :  ∀ m n → m + suc n ≡ suc m + n                                       
n≢1+n : ∀ {n} → n ≢ suc n                                                                             
1<2+n :  ∀ n → 1 < 2 + n                                                                                                                                  
<1⇒≡0 :  ∀ {n} → n < 1 → n ≡ 0                                                    
n≤1⇒n≡0∨n≡1 : ∀ {n} → n ≤ 1 → n ≡ 0 ⊎ n ≡ 1                                       
m<n⇒0<n : ∀ {m n} → m < n → 0 < n                                                                                                                        
pred-n≤n : ∀ {n} → pred n ≤ n                                                                                        
m≤n*m : ∀ m {n} → 0 < n → m ≤ n * m                                
m<n⇒n∸m>0 :  {m n : ℕ} → m < n → n ∸ m > 0
m*[1+n] :  ∀ m n → m * (suc n) ≡ m + m * n 

There are also possible for Nat(Integer): upFrom, upTo, downFrom, from_to_,
with their properties in ..Properties:

upTo-n≤n :  ∀ n → All (_≤ n) (upTo n)
length-upFrom : ∀ n c → length (upFrom n c) ≡ suc c
length-from-to :  ∀ m n → length (from m to n) ≡ suc (n ∸ m) 

?

[mechvel]

May be, this one is useful:

pred-n<n : ∀ {n} → n ≢ 0 → pred n < n
pred-n<n {suc n} _   =  ≤-refl
pred-n<n {0}     0≢0 =  contradiction refl 0≢0

[gallais]

m+suc[n]≡suc[m]+n : ∀ m n → m + suc n ≡ suc m + n

already exists: +-suc : ∀ m n → m + suc n ≡ suc (m + n)

Edit: I'll only list the ones that already exist in the big list in the top message
rather than updating both.

Edit: not sure what from_to_ is supposed to be? Same question for upFrom.

[MatthewDaggitt]

Opened #2087 to deal with the naming issue. I'm with @gallais in not understanding what the last two lemmas are supposed to be, and it's been two years with no reply so I'm going to close this one.