欧几里得算法   gcd(a,b)=gcd(b,a mod(b));

　  $start:

　　　  hypo: r=a mod b,  d=gcd(a,b);

　  　　$: a=kb+r;   　　　 　

　  　　$: r/d= a/d-(kb)/d;

　 　　 $: r mod d=0;

     　　$: if d=gcd(a,b) then d <- gcd(r);

　　　  $: if d=gcd(a,b) then  d|r; 

　　　  hypo:  A=gcd(a,b) :set;  B= gcd(b,r) :set; C=gcd(a,r) :set;

　　　  $: A<- B && A<- C;

　　　　hypo:  d‘=gcd(b,r);

　　　  $: a/d‘= kb/d‘ +r/d‘;

　　　  $: d‘|a $: B<-A;

　　　  $:A=B;　　　　　　　　　　　　　　

     $end; 

欧几里得算法(辗转相除法)