cong_intro

Theorem cong_intro

Theorem. cong_intro
k ∈ ℤ → a - b = m⋅k → cong a b m

Proof
01. 1 ⊢ k ∈ ℤ, hypo.
02. 2 ⊢ a - b = m⋅k, hypo.
03. 1, 2 ⊢ k ∈ ℤ ∧ a - b = m⋅k, conj_intro 1 2.
04. 1, 2 ⊢ ∃k. k ∈ ℤ ∧ a - b = m⋅k, ex_intro 3.
05. ⊢ divides m (a - b) ↔ ∃k. k ∈ ℤ ∧ a - b = m⋅k, divides_equi.
06. 1, 2 ⊢ divides m (a - b), rsubj_elim 5 4.
07. 1, 2 ⊢ cong a b m, rsubj_elim cong_equi 6.
cong_intro. ⊢ k ∈ ℤ → a - b = m⋅k → cong a b m, subj_intro_ii 7.