α : Type ?u.268594
β : Type ?u.268597
γ : Type ?u.268600
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c
α : Type ?u.268594
β : Type ?u.268597
γ : Type ?u.268600
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : c ∣ b
⊢ a % b % c = a % c
nth_rw 2 [← div_add_mod a b]
case intro
α : Type ?u.268594
β : Type ?u.268597
γ : Type ?u.268600
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a c d : Ordinal
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c
α : Type ?u.268594
β : Type ?u.268597
γ : Type ?u.268600
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c
rcases h with ⟨d, rfl⟩
no goals
case intro
α : Type ?u.268594
β : Type ?u.268597
γ : Type ?u.268600
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a c d : Ordinal
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c
rw [mul_assoc, mul_add_mod_self]