Step
*
2
of Lemma
gcd_p_neg_arg_2
1. a : ℤ
2. b : ℤ
3. y : ℤ
4. GCD(a;-b;y)
⊢ GCD(a;b;y)
BY
{ (RWH (IfIsC ⌜b⌝ (RevLemmaC `minus_minus_cancel`)) 0 THENA Auto) }
1
1. a : ℤ
2. b : ℤ
3. y : ℤ
4. GCD(a;-b;y)
⊢ GCD(a;--b;y)
Latex:
Latex:
1. a : \mBbbZ{}
2. b : \mBbbZ{}
3. y : \mBbbZ{}
4. GCD(a;-b;y)
\mvdash{} GCD(a;b;y)
By
Latex:
(RWH (IfIsC \mkleeneopen{}b\mkleeneclose{} (RevLemmaC `minus\_minus\_cancel`)) 0 THENA Auto)
Home
Index