---

Step * 1 2 1 of Lemma div_rem_gcd_anne


1. m : @i
2. n : @i
3. g : @i
4. GCD(n;m rem n;g)@i
 GCD(m;n;g)
BY
{ All(Unfold `gcd_p`) }

1
1. m : @i
2. n : @i
3. g : @i
4. (g | n)  (g | (m rem n))  (z:. (((z | n)  (z | (m rem n)))  (z | g)))@i
 (g | m)  (g | n)  (z:. (((z | m)  (z | n))  (z | g)))



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


By

All(Unfold  `gcd\_p`)\mcdot{}



Home Index