fact: Definition Gcd gcd x y := If x = 0 then y else If y = 0 then x else If x <= y then gcd x (y-x) else gcd (x-y) y.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat