---

Step * 1 1 of Lemma div_rem_gcd_anne


1. m : @i
2. n : @i
3. g : @i
 GCD(m;n;g)  GCD(n;m rem n;g)
BY
{ (D 0 THENA Auto) }

1
1. m : @i
2. n : @i
3. g : @i
4. GCD(m;n;g)@i
 GCD(n;m rem n;g)



1.  m  :  \mBbbZ{}@i
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}@i
3.  g  :  \mBbbZ{}@i
\mvdash{}  GCD(m;n;g)  {}\mRightarrow{}  GCD(n;m  rem  n;g)


By

(D  0  THENA  Auto)



Home Index