Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Mario Carneiro
-/
import Std.Data.Int.Lemmas
/-!
# Lemmas about integer division
-/
open Nat
namespace Int
/-! ### `/` -/
theorem ofNat_div : ∀ (m n : Nat ), ↑(m / n = div ↑m ↑n ofNat_div ( m n : Nat ) : ↑( m / n ) = div ↑ m ↑ n := rfl : ∀ {α : Sort ?u.133} {a : α }, a = a
theorem ofNat_fdiv : ∀ (m n : Nat ), ↑(m / n = fdiv ↑m ↑n ofNat_fdiv : ∀ m n : Nat , ↑( m / n ) = fdiv ↑ m ↑ n
| 0 , _ => by simp [ fdiv ]
| succ _, _ => rfl : ∀ {α : Sort ?u.330} {a : α }, a = a
@[ simp , norm_cast ] theorem ofNat_ediv : ∀ (m n : Nat ), ↑(m / n = ↑m / ↑n ofNat_ediv ( m n : Nat ) : (↑( m / n ) : Int ) = ↑ m / ↑ n := rfl : ∀ {α : Sort ?u.673} {a : α }, a = a
theorem negSucc_ediv ( m : Nat ) { b : Int } ( H : 0 < b ) : -[ m +1] / b = -( div m b + 1 ) :=
match b , eq_succ_of_zero_lt : ∀ {a : Int }, 0 < a ∃ n , a = ↑(succ n H with
| _, ⟨ _ , rfl : ∀ {α : Sort ?u.964} {a : α }, a = a ⟩ => rfl : ∀ {α : Sort ?u.1024} {a : α }, a = a
@[ simp ] protected theorem zero_div : ∀ b : Int , div 0 b = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => show - ofNat _ = _ by simp
@[ local simp ] theorem zero_ediv : ∀ (b : Int ), 0 / b = 0 zero_ediv : ∀ b : Int , 0 / b = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => show - ofNat _ = _ by simp
@[ simp ] theorem zero_fdiv ( b : Int ) : fdiv 0 b = 0 := by cases b <;> rfl
@[ simp ] protected theorem div_zero : ∀ a : Int , div a 0 = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => rfl : ∀ {α : Sort ?u.2925} {a : α }, a = a
-- Will be generalized to Euclidean domains.
@[ local simp ] protected theorem ediv_zero : ∀ (a : Int ), a / 0 = 0 ediv_zero : ∀ a : Int , a / 0 = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => rfl : ∀ {α : Sort ?u.3242} {a : α }, a = a
@[ simp ] protected theorem fdiv_zero : ∀ a : Int , fdiv a 0 = 0
| 0 => rfl : ∀ {α : Sort ?u.3423} {a : α }, a = a
| succ _ => rfl : ∀ {α : Sort ?u.3496} {a : α }, a = a
| -[_+1] => rfl : ∀ {α : Sort ?u.3545} {a : α }, a = a
theorem fdiv_eq_ediv : ∀ ( a : Int ) { b : Int }, 0 ≤ b → fdiv a b = a / b
| 0 , _, _ | -[_+1], 0 , _ => by simp
| succ _, ofNat _, _ | -[_+1], succ _, _ => rfl : ∀ {α : Sort ?u.3951} {a : α }, a = a
theorem div_eq_ediv : ∀ {a b : Int }, 0 ≤ a 0 ≤ b div a b = a / b div_eq_ediv : ∀ { a b : Int }, 0 ≤ a → 0 ≤ b → a . div b = a / b
| 0 , _, _, _ | _, 0 , _, _ => by x✝² : Int x✝¹ : 0 ≤ x✝² x✝ : 0 ≤ 0 simp
| succ _, succ _, _, _ => rfl : ∀ {α : Sort ?u.4884} {a : α }, a = a
theorem fdiv_eq_div { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : fdiv a b = div a b :=
div_eq_ediv : ∀ {a b : Int }, 0 ≤ a 0 ≤ b div a b = a / b Ha Hb ▸ fdiv_eq_ediv _ Hb
@[ simp ] protected theorem div_neg : ∀ a b : Int , a . div (- b ) = -( a . div b )
| ofNat m , 0 => show ofNat ( m / 0 ) = -↑( m / 0 ) by rw [ Nat.div_zero : ∀ (n : Nat ), n / 0 = 0 ] ; rfl
| ofNat m , -[ n +1] | -[ m +1], succ n => ( Int.neg_neg : ∀ (a : Int ), - - a = a _ ). symm : ∀ {α : Sort ?u.6519} {a b : α }, a = b b = a symm
| ofNat m , succ n | -[ m +1], 0 | -[ m +1], -[ n +1] => rfl : ∀ {α : Sort ?u.6731} {a : α }, a = a
@[ simp ] protected theorem ediv_neg : ∀ (a b : Int ), a / - b = - (a / b ediv_neg : ∀ a b : Int , a / (- b ) = -( a / b )
| ofNat m , 0 => show ofNat ( m / 0 ) = -↑( m / 0 ) by rw [ Nat.div_zero : ∀ (n : Nat ), n / 0 = 0 ] ; rfl
| ofNat m , -[ n +1] => ( Int.neg_neg : ∀ (a : Int ), - - a = a _ ). symm : ∀ {α : Sort ?u.7352} {a b : α }, a = b b = a symm
| ofNat m , succ n | -[ m +1], 0 | -[ m +1], succ n | -[ m +1], -[ n +1] => rfl : ∀ {α : Sort ?u.7707} {a : α }, a = a
protected theorem div_def ( a b : Int ) : a / b = Int.ediv a b := rfl : ∀ {α : Sort ?u.8063} {a : α }, a = a
-- Lean 4 core provides an instance for `Div Int` using `Int.div`.
-- Even though we provide a higher priority instance in `Std.Data.Int.Basic`,
-- we provide a `simp` lemma here to unfold usages of that instance back to `Int.div`.
@[ simp ] theorem div_def' : ∀ (a b : Int ), a / b = div a b div_def' ( a b : Int ) :
@ HDiv.hDiv Int Int Int (@ instHDiv : {α : Type ?u.8080} → [inst : Div α HDiv α α α Int Int.instDivInt ) a b = Int.div a b := rfl : ∀ {α : Sort ?u.8089} {a : α }, a = a
@[ simp ] protected theorem neg_div : ∀ a b : Int , (- a ). div b = -( a . div b )
| 0 , n => by simp [ Int.neg_zero ]
| succ m , (n:Nat) | -[ m +1], 0 | -[ m +1], -[ n +1] => rfl : ∀ {α : Sort ?u.8303} {a : α }, a = a
| succ m , -[ n +1] | -[ m +1], succ n => ( Int.neg_neg : ∀ (a : Int ), - - a = a _ ). symm : ∀ {α : Sort ?u.8546} {a b : α }, a = b b = a symm
protected theorem neg_div_neg ( a b : Int ) : (- a ). div (- b ) = a . div b := by
simp [ Int.div_neg , Int.neg_div , Int.neg_neg : ∀ (a : Int ), - - a = a ]
protected theorem div_nonneg : ∀ {a b : Int }, 0 ≤ a 0 ≤ b 0 ≤ div a b div_nonneg { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : 0 ≤ a . div b :=
match a , b , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n Ha , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n Hb with
| _, _, ⟨ _ , rfl : ∀ {α : Sort ?u.9393} {a : α }, a = a ⟩, ⟨ _ , rfl : ∀ {α : Sort ?u.9397} {a : α }, a = a ⟩ => ofNat_zero_le : ∀ (n : Nat ), 0 ≤ ↑n _
theorem fdiv_nonneg : ∀ {a b : Int }, 0 ≤ a 0 ≤ b 0 ≤ fdiv a b fdiv_nonneg { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : 0 ≤ a . fdiv b :=
match a , b , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n Ha , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n Hb with
| _, _, ⟨ _ , rfl : ∀ {α : Sort ?u.10023} {a : α }, a = a ⟩, ⟨ _ , rfl : ∀ {α : Sort ?u.10027} {a : α }, a = a ⟩ => ofNat_fdiv : ∀ (m n : Nat ), ↑(m / n = fdiv ↑m ↑n .. ▸ ofNat_zero_le : ∀ (n : Nat ), 0 ≤ ↑n _
theorem ediv_nonneg : ∀ {a b : Int }, 0 ≤ a 0 ≤ b 0 ≤ a / b ediv_nonneg { a b : Int } ( Ha : 0 ≤ a ) ( Hb : 0 ≤ b ) : 0 ≤ a / b :=
match a , b , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n Ha , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n Hb with
| _, _, ⟨ _ , rfl : ∀ {α : Sort ?u.10648} {a : α }, a = a ⟩, ⟨ _ , rfl : ∀ {α : Sort ?u.10652} {a : α }, a = a ⟩ => ofNat_zero_le : ∀ (n : Nat ), 0 ≤ ↑n _
protected theorem div_nonpos : ∀ {a b : Int }, 0 ≤ a b ≤ 0 div a b ≤ 0 div_nonpos { a b : Int } ( Ha : 0 ≤ a ) ( Hb : b ≤ 0 ) : a . div b ≤ 0 :=
Int.nonpos_of_neg_nonneg : ∀ {a : Int }, 0 ≤ - a a ≤ 0 <| Int.div_neg .. ▸ Int.div_nonneg : ∀ {a b : Int }, 0 ≤ a 0 ≤ b 0 ≤ div a b Ha ( Int.neg_nonneg_of_nonpos : ∀ {a : Int }, a ≤ 0 0 ≤ - a Hb )
theorem fdiv_nonpos : ∀ {a b : Int }, 0 ≤ a b ≤ 0 fdiv a b ≤ 0 fdiv_nonpos : ∀ { a b : Int }, 0 ≤ a → b ≤ 0 → a . fdiv b ≤ 0
| 0 , 0 , _, _ | 0 , -[_+1], _, _ | succ _, 0 , _, _ | succ _, -[_+1], _, _ => ⟨ _ ⟩
theorem ediv_nonpos : ∀ {a b : Int }, 0 ≤ a b ≤ 0 a / b ≤ 0 ediv_nonpos { a b : Int } ( Ha : 0 ≤ a ) ( Hb : b ≤ 0 ) : a / b ≤ 0 :=
Int.nonpos_of_neg_nonneg : ∀ {a : Int }, 0 ≤ - a a ≤ 0 <| Int.ediv_neg : ∀ (a b : Int ), a / - b = - (a / b .. ▸ Int.ediv_nonneg : ∀ {a b : Int }, 0 ≤ a 0 ≤ b 0 ≤ a / b Ha ( Int.neg_nonneg_of_nonpos : ∀ {a : Int }, a ≤ 0 0 ≤ - a Hb )
theorem fdiv_neg' : ∀ {a b : Int }, a < 0 0 < b fdiv a b < 0 fdiv_neg' : ∀ { a b : Int }, a < 0 → 0 < b → a . fdiv b < 0
| -[_+1], succ _, _, _ => negSucc_lt_zero _
theorem ediv_neg' : ∀ {a b : Int }, a < 0 0 < b a / b < 0 ediv_neg' { a b : Int } ( Ha : a < 0 ) ( Hb : 0 < b ) : a / b < 0 :=
match a , b , eq_negSucc_of_lt_zero : ∀ {a : Int }, a < 0 ∃ n , a = -[ n +1] Ha , eq_succ_of_zero_lt : ∀ {a : Int }, 0 < a ∃ n , a = ↑(succ n Hb with
| _, _, ⟨ _ , rfl : ∀ {α : Sort ?u.14653} {a : α }, a = a ⟩, ⟨ _ , rfl : ∀ {α : Sort ?u.14657} {a : α }, a = a ⟩ => negSucc_lt_zero _
@[ simp ] protected theorem div_one : ∀ a : Int , a . div 1 = a
| (n:Nat) => congrArg : ∀ {α : Sort ?u.15243} {β : Sort ?u.15242} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ ofNat ( Nat.div_one : ∀ (n : Nat ), n / 1 = n _ )
| -[ n +1] => by simp [ Int.div , neg_ofNat_succ ]
@[ simp ] theorem fdiv_one : ∀ a : Int , a . fdiv 1 = a
| 0 => rfl : ∀ {α : Sort ?u.15533} {a : α }, a = a
| succ _ => congrArg : ∀ {α : Sort ?u.15607} {β : Sort ?u.15606} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ Nat.cast ( Nat.div_one : ∀ (n : Nat ), n / 1 = n _ )
| -[_+1] => congrArg : ∀ {α : Sort ?u.15663} {β : Sort ?u.15662} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ negSucc ( Nat.div_one : ∀ (n : Nat ), n / 1 = n _ )
@[ simp ] theorem ediv_one : ∀ (a : Int ), a / 1 = a ediv_one : ∀ a : Int , a / 1 = a
| (_:Nat) => congrArg : ∀ {α : Sort ?u.15900} {β : Sort ?u.15899} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ Nat.cast ( Nat.div_one : ∀ (n : Nat ), n / 1 = n _ )
| -[_+1] => congrArg : ∀ {α : Sort ?u.15964} {β : Sort ?u.15963} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ negSucc ( Nat.div_one : ∀ (n : Nat ), n / 1 = n _ )
theorem div_eq_zero_of_lt : ∀ {a b : Int }, 0 ≤ a a < b div a b = 0 div_eq_zero_of_lt { a b : Int } ( H1 : 0 ≤ a ) ( H2 : a < b ) : a . div b = 0 :=
match a , b , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n H1 , eq_succ_of_zero_lt : ∀ {a : Int }, 0 < a ∃ n , a = ↑(succ n ( Int.lt_of_le_of_lt : ∀ {a b c : Int }, a ≤ b b < c a < c H1 H2 ) with
| _, _, ⟨ _ , rfl : ∀ {α : Sort ?u.16151} {a : α }, a = a ⟩, ⟨ _ , rfl : ∀ {α : Sort ?u.16163} {a : α }, a = a ⟩ => congrArg : ∀ {α : Sort ?u.16261} {β : Sort ?u.16260} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ Nat.cast <| Nat.div_eq_of_lt : ∀ {a b : Nat }, a < b a / b = 0 <| ofNat_lt : ∀ {n m : Nat }, ↑n < ↑m ↔ n < m . 1 : ∀ {a b : Prop }, (a ↔ b a → b H2
theorem ediv_eq_zero_of_lt : ∀ {a b : Int }, 0 ≤ a a < b a / b = 0 ediv_eq_zero_of_lt { a b : Int } ( H1 : 0 ≤ a ) ( H2 : a < b ) : a / b = 0 :=
match a , b , eq_ofNat_of_zero_le : ∀ {a : Int }, 0 ≤ a ∃ n , a = ↑n H1 , eq_succ_of_zero_lt : ∀ {a : Int }, 0 < a ∃ n , a = ↑(succ n ( Int.lt_of_le_of_lt : ∀ {a b c : Int }, a ≤ b b < c a < c H1 H2 ) with
| _, _, ⟨ _ , rfl : ∀ {α : Sort ?u.16838} {a : α }, a = a ⟩, ⟨ _ , rfl : ∀ {α : Sort ?u.16842} {a : α }, a = a ⟩ => congrArg : ∀ {α : Sort ?u.16940} {β : Sort ?u.16939} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ Nat.cast <| Nat.div_eq_of_lt : ∀ {a b : Nat }, a < b a / b = 0 <| ofNat_lt : ∀ {n m : Nat }, ↑n < ↑m ↔ n < m . 1 : ∀ {a b : Prop }, (a ↔ b a → b H2
theorem add_mul_ediv_right : ∀ (a b : Int ) {c : Int }, c ≠ 0 (a + b * c / c = a / c + b add_mul_ediv_right ( a b : Int ) { c : Int } ( H : c ≠ 0 ) : ( a + b * c ) / c = a / c + b :=
suffices ∀ {{ a b c : Int }}, 0 < c → ( a + b * c ). ediv c = a . ediv c + b from
match Int.lt_trichotomy : ∀ (a b : Int ), a < b ∨ a = b ∨ b < a c 0 with
| Or.inl : ∀ {a b : Prop }, a → a ∨ b hlt => by
rw [ ← Int.neg_inj : ∀ {a b : Int }, - a = - b ↔ a = b , ← Int.ediv_neg : ∀ (a b : Int ), a / - b = - (a / b , Int.neg_add : ∀ {a b : Int }, - (a + b = - a + - b , ← Int.ediv_neg : ∀ (a b : Int ), a / - b = - (a / b , ← Int.neg_mul_neg : ∀ (a b : Int ), - a * - b = a * b ]
exact this ( Int.neg_pos_of_neg : ∀ {a : Int }, a < 0 0 < - a hlt )
| Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b HEq ) => absurd : ∀ {a : Prop } {b : Sort ?u.19344}, a → ¬ a b HEq H
| Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inr : ∀ {a b : Prop }, b → a ∨ b hgt ) => this hgt
suffices ∀ { k n : Nat } { a : Int }, ( a + n * k . succ ). ediv k . succ = a . ediv k . succ + n from
fun a b c H => match c , eq_succ_of_zero_lt : ∀ {a : Int }, 0 < a ∃ n , a = ↑(succ n H , b with
| _, ⟨ _ , rfl : ∀ {α : Sort ?u.18106} {a : α }, a = a ⟩, ofNat _ => this
| _, ⟨ k , rfl : ∀ {α : Sort ?u.18181} {a : α }, a = a ⟩, -[ n +1] => show ( a - n . succ * k . succ ). ediv k . succ = a . ediv k . succ - n . succ by
rw [ ← Int.add_sub_cancel : ∀ (a b : Int ), a + b - b = a ( ediv ..), ← this , Int.sub_add_cancel : ∀ (a b : Int ), a - b + b = a ]
fun { k n } => @ fun
| ofNat m => congrArg : ∀ {α : Sort ?u.17877} {β : Sort ?u.17876} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ ofNat <| Nat.add_mul_div_right : ∀ (x y : Nat ) {z : Nat }, 0 < z (x + y * z / z = x / z + y _ _ k . succ_pos
| -[ m +1] => by
show (( n * k . succ : Nat ) - m . succ : Int ). ediv k . succ = n - ( m / k . succ + 1 : Nat )
if h : m < n * k . succ then
rw [ ← Int.ofNat_sub : ∀ {m n : Nat }, m ≤ n ↑(n - m = ↑n - ↑m h , ← Int.ofNat_sub : ∀ {m n : Nat }, m ≤ n ↑(n - m = ↑n - ↑m (( Nat.div_lt_iff_lt_mul : ∀ {k x y : Nat }, 0 < k x / k < y ↔ x < y * k k . succ_pos ). 2 : ∀ {a b : Prop }, (a ↔ b b → a h ) ]
apply congrArg : ∀ {α : Sort ?u.20781} {β : Sort ?u.20780} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ ofNat
rw [ Nat.mul_comm : ∀ (n m : Nat ), n * m = m * n , Nat.mul_sub_div ] ; rwa [ Nat.mul_comm : ∀ (n m : Nat ), n * m = m * n ]
else
have h := Nat.not_lt : ∀ {a b : Nat }, ¬ a < b ↔ b ≤ a . 1 : ∀ {a b : Prop }, (a ↔ b a → b h
have H { a b : Nat } ( h : a ≤ b ) : ( a : Int ) + -(( b : Int ) + 1 ) = -[ b - a +1] := by
rw [ negSucc_eq , Int.ofNat_sub : ∀ {m n : Nat }, m ≤ n ↑(n - m = ↑n - ↑m h ]
simp only [ Int.sub_eq_add_neg : ∀ {a b : Int }, a - b = a + - b , Int.neg_add : ∀ {a b : Int }, - (a + b = - a + - b , Int.neg_neg : ∀ (a : Int ), - - a = a , Int.add_left_comm : ∀ (a b c : Int ), a + (b + c = b + (a + c , Int.add_assoc : ∀ (a b c : Int ), a + b + c = a + (b + c ]
show ediv (↑( n * succ k ) + -(( m : Int ) + 1 )) ( succ k ) = n + -(↑( m / succ k ) + 1 : Int )
rw [ H h , H (( Nat.le_div_iff_mul_le : ∀ {k x y : Nat }, 0 < k x ≤ y / k ↔ x * k ≤ y k . succ_pos ). 2 : ∀ {a b : Prop }, (a ↔ b b → a h ) ]
apply congrArg : ∀ {α : Sort ?u.22422} {β : Sort ?u.22421} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ negSucc
rw [ Nat.mul_comm : ∀ (n m : Nat ), n * m = m * n , Nat.sub_mul_div : ∀ (x n p : Nat ), n * p ≤ x (x - n * p / n = x / n - p ] ; rwa [ Nat.mul_comm : ∀ (n m : Nat ), n * m = m * n ]
theorem add_mul_ediv_left : ∀ (a : Int ) {b : Int } (c : Int ), b ≠ 0 (a + b * c / b = a / b + c add_mul_ediv_left ( a : Int ) { b : Int }
( c : Int ) ( H : b ≠ 0 ) : ( a + b * c ) / b = a / b + c :=
Int.mul_comm : ∀ (a b : Int ), a * b = b * a .. ▸ Int.add_mul_ediv_right : ∀ (a b : Int ) {c : Int }, c ≠ 0 (a + b * c / c = a / c + b _ _ H
theorem add_ediv_of_dvd_right : ∀ {a b c : Int }, c ∣ b (a + b / c = a / c + b / c add_ediv_of_dvd_right { a b c : Int } ( H : c ∣ b ) : ( a + b ) / c = a / c + b / c :=
if h : c = 0 then by a, b, c : Int H : c ∣ b h : c = 0 simp [ h ] else by
let ⟨ k , hk ⟩ := H
rw [ hk , Int.mul_comm : ∀ (a b : Int ), a * b = b * a c k , Int.add_mul_ediv_right : ∀ (a b : Int ) {c : Int }, c ≠ 0 (a + b * c / c = a / c + b _ _ h ,
← Int.zero_add : ∀ (a : Int ), 0 + a = a ( k * c ), Int.add_mul_ediv_right : ∀ (a b : Int ) {c : Int }, c ≠ 0 (a + b * c / c = a / c + b _ _ h , Int.zero_ediv : ∀ (b : Int ), 0 / b = 0 , Int.zero_add : ∀ (a : Int ), 0 + a = a ]
theorem add_ediv_of_dvd_left : ∀ {a b c : Int }, c ∣ a (a + b / c = a / c + b / c add_ediv_of_dvd_left { a b c : Int } ( H : c ∣ a ) : ( a + b ) / c = a / c + b / c := by
rw [ Int.add_comm : ∀ (a b : Int ), a + b = b + a , Int.add_ediv_of_dvd_right : ∀ {a b c : Int }, c ∣ b (a + b / c = a / c + b / c H , Int.add_comm : ∀ (a b : Int ), a + b = b + a ]
@[ simp ] theorem mul_ediv_cancel : ∀ (a : Int ) {b : Int }, b ≠ 0 a * b / b = a mul_ediv_cancel ( a : Int ) { b : Int } ( H : b ≠ 0 ) : ( a * b ) / b = a := by
have := Int.add_mul_ediv_right : ∀ (a b : Int ) {c : Int }, c ≠ 0 (a + b * c / c = a / c + b 0 a H a, b : Int H : b ≠ 0 this : (0 + a * b / b = 0 / b + a
rwa [ a, b : Int H : b ≠ 0 this : (0 + a * b / b = 0 / b + a Int.zero_add : ∀ (a : Int ), 0 + a = a , a, b : Int H : b ≠ 0 this : (0 + a * b / b = 0 / b + a Int.zero_ediv : ∀ (b : Int ), 0 / b = 0 , a, b : Int H : b ≠ 0 this : a * b / b = 0 + a a, b : Int H : b ≠ 0 this : (0 + a * b / b = 0 / b + a Int.zero_add : ∀ (a : Int ), 0 + a = a a, b : Int H : b ≠ 0 this : a * b / b = a ] a, b : Int H : b ≠ 0 this : a * b / b = a at this : a * b / b = 0 / b + a this
@[ simp ] theorem mul_fdiv_cancel : ∀ (a : Int ) {b : Int }, b ≠ 0 fdiv (a * b b = a mul_fdiv_cancel ( a : Int ) { b : Int } ( H : b ≠ 0 ) : fdiv ( a * b ) b = a :=
if b0 : 0 ≤ b then by
a, b : Int H : b ≠ 0 b0 : 0 ≤ b rw [ a, b : Int H : b ≠ 0 b0 : 0 ≤ b fdiv_eq_ediv _ b0 , a, b : Int H : b ≠ 0 b0 : 0 ≤ b a, b : Int H : b ≠ 0 b0 : 0 ≤ b mul_ediv_cancel : ∀ (a : Int ) {b : Int }, b ≠ 0 a * b / b = a _ H a, b : Int H : b ≠ 0 b0 : 0 ≤ b ]
else
match a , b , Int.not_le : ∀ {a b : Int }, ¬ a ≤ b ↔ b < a . 1 : ∀ {a b : Prop }, (a ↔ b a → b b0 with
| 0 , _, _ => by a, b, x✝¹ : Int x✝ : x✝¹ < 0 H : x✝¹ ≠ 0 b0 : ¬ 0 ≤ x✝¹ simp [ Int.zero_mul : ∀ (a : Int ), 0 * a = 0 ]
| succ a , -[ b +1], _ => congrArg : ∀ {α : Sort ?u.24313} {β : Sort ?u.24312} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ ofNat <| Nat.mul_div_cancel : ∀ (m : Nat ) {n : Nat }, 0 < n m * n / n = m ( succ a ) b . succ_pos
| -[ a +1], -[ b +1], _ => congrArg : ∀ {α : Sort ?u.24622} {β : Sort ?u.24621} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ negSucc <| Nat.div_eq_of_lt_le : ∀ {k n m : Nat }, k * n ≤ m m < succ k * n m / n = k
( le_of_lt_succ : ∀ {m n : Nat }, m < succ n m ≤ n <| Nat.mul_lt_mul_of_pos_right : ∀ {n m k : Nat }, n < m k > 0 n * k < m * k a . lt_succ_self b . succ_pos )
( lt_succ_self _ )
@[ simp ] protected theorem mul_div_cancel : ∀ (a : Int ) {b : Int }, b ≠ 0 div (a * b b = a mul_div_cancel ( a : Int ) { b : Int } ( H : b ≠ 0 ) : ( a * b ). div b = a :=
have : ∀ { a b : Nat }, ( b : Int ) ≠ 0 → ( div ( a * b ) b : Int ) = a := fun H => by
div (↑a✝ * ↑b✝ ↑b✝ = ↑a✝ rw [ div (↑a✝ * ↑b✝ ↑b✝ = ↑a✝ ← ofNat_mul : ∀ (n m : Nat ), ↑(n * m = ↑n * ↑m , div (↑a✝ * ↑b✝ ↑b✝ = ↑a✝ ← ofNat_div : ∀ (m n : Nat ), ↑(m / n = div ↑m ↑n ,
div (↑a✝ * ↑b✝ ↑b✝ = ↑a✝ Nat.mul_div_cancel : ∀ (m : Nat ) {n : Nat }, 0 < n m * n / n = m _ <| Nat.pos_of_ne_zero : ∀ {n : Nat }, n ≠ 0 0 < n <| Int.ofNat_ne_zero : ∀ {n : Nat }, ↑n ≠ 0 ↔ n ≠ 0 . 1 : ∀ {a b : Prop }, (a ↔ b a → b H ]
match a , b , a . eq_nat_or_neg : ∀ (a : Int ), ∃ n , a = ↑n ∨ a = - ↑n , b . eq_nat_or_neg : ∀ (a : Int ), ∃ n , a = ↑n ∨ a = - ↑n with
| _, _, ⟨ a , .inl : ∀ {a b : Prop }, a → a ∨ b rfl : ∀ {α : Sort ?u.25840} {a : α }, a = a ⟩, ⟨ b , .inl : ∀ {a b : Prop }, a → a ∨ b rfl : ∀ {α : Sort ?u.25844} {a : α }, a = a ⟩ => this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a this H
| _, _, ⟨ a , .inl : ∀ {a b : Prop }, a → a ∨ b rfl : ∀ {α : Sort ?u.25983} {a : α }, a = a ⟩, ⟨ b , .inr : ∀ {a b : Prop }, b → a ∨ b rfl : ∀ {α : Sort ?u.25987} {a : α }, a = a ⟩ => by
rw [ Int.mul_neg : ∀ (a b : Int ), a * - b = - (a * b , Int.neg_div , Int.div_neg , Int.neg_neg : ∀ (a : Int ), - - a = a ,
this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a this ( Int.neg_ne_zero : ∀ {a : Int }, - a ≠ 0 ↔ a ≠ 0 . 1 : ∀ {a b : Prop }, (a ↔ b a → b H ) ]
| _, _, ⟨ a , .inr : ∀ {a b : Prop }, b → a ∨ b rfl : ∀ {α : Sort ?u.26066} {a : α }, a = a ⟩, ⟨ b , .inl : ∀ {a b : Prop }, a → a ∨ b rfl : ∀ {α : Sort ?u.26070} {a : α }, a = a ⟩ => by a✝, b✝ : Int this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a a, b : Nat H : ↑b ≠ 0 rw [ a✝, b✝ : Int this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a a, b : Nat H : ↑b ≠ 0 Int.neg_mul : ∀ (a b : Int ), - a * b = - (a * b , a✝, b✝ : Int this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a a, b : Nat H : ↑b ≠ 0 a✝, b✝ : Int this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a a, b : Nat H : ↑b ≠ 0 Int.neg_div , a✝, b✝ : Int this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a a, b : Nat H : ↑b ≠ 0 a✝, b✝ : Int this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a a, b : Nat H : ↑b ≠ 0 this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a this H a✝, b✝ : Int this : ∀ {a b : Nat }, ↑b ≠ 0 div (↑a * ↑b ↑b = ↑a a, b : Nat H : ↑b ≠ 0 ]
| _, _, ⟨ a , .inr : ∀ {a b : Prop }, b → a ∨ b rfl : ∀ {α : Sort ?u.26149} {a : α }, a = a ⟩, ⟨ b , .inr : ∀ {a b : Prop }, b → a ∨ b rfl : ∀ {α : Sort ?u.26153} {a : α }, a = a ⟩ => by
rw [ Int.neg_mul_neg : ∀ (a b : Int ), - a * - b = a * b , Int.div_neg ,