cong_elim

Theorem cong_elim

Theorem. cong_elim
cong a b m → ∃k. k ∈ ℤ ∧ (a - b) = m⋅k

Proof
01. 1 ⊢ cong a b m, hypo.
02. 1 ⊢ divides m (a - b), lsubj_elim cong_equi 1.
03. ⊢ divides m (a - b) ↔ ∃k. k ∈ ℤ ∧ (a - b) = m⋅k, divides_equi.
04. 1 ⊢ ∃k. k ∈ ℤ ∧ (a - b) = m⋅k, lsubj_elim 3 2.
cong_elim. ⊢ cong a b m → ∃k. k ∈ ℤ ∧ (a - b) = m⋅k, subj_intro 4.