Step
*
1
of Lemma
bezout_sq_exists_anne
1. n : 
@i
 
m:
. (
p:{
 
 
| let x,y = p in GCD(m;n;(x * m) + (y * n))})
BY
{ (GeneralNatInd 1 THENA Auto) }
1
1. n : 
@i
2. 
n1:
n. 
m:
.  (
p:{
 
 
| let x,y = p in GCD(m;n1;(x * m) + (y * n1))})@i
 
m:
. (
p:{
 
 
| let x,y = p in GCD(m;n;(x * m) + (y * n))})
1.  n  :  \mBbbN{}@i
\mvdash{}  \mforall{}m:\mBbbN{}.  (\mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  x,y  =  p  in  GCD(m;n;(x  *  m)  +  (y  *  n))\})
By
(GeneralNatInd  1  THENA  Auto)
Home
Index