---

Step * 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 }

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

2
1. m : @i
2. n : @i
3. g : @i
 GCD(m;n;g)  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)  \mLeftarrow{}{}\mRightarrow{}  GCD(n;m  rem  n;g)


By

D  0



Home Index