Step
*
2
of Lemma
add_reduce_eqmod
1. m : ℤ
2. x : ℤ
3. y : ℤ
4. y ≡ 0 mod m
⊢ (x + y) ≡ x mod m
BY
{ (Assert ⌜x ≡ x mod m⌝⋅ THENA (RelRST THEN Auto)) }
1
1. m : ℤ
2. x : ℤ
3. y : ℤ
4. y ≡ 0 mod m
5. x ≡ x mod m
⊢ (x + y) ≡ x mod m
Latex:
Latex:
1. m : \mBbbZ{}
2. x : \mBbbZ{}
3. y : \mBbbZ{}
4. y \mequiv{} 0 mod m
\mvdash{} (x + y) \mequiv{} x mod m
By
Latex:
(Assert \mkleeneopen{}x \mequiv{} x mod m\mkleeneclose{}\mcdot{} THENA (RelRST THEN Auto))
Home
Index