fact: Definition gcd_gt_body a b cont := match compare b zero with | Gt => let r := mod_gt a b in match compare r zero with | Gt => cont r (mod_gt b r) | _ => b end | _ => a end.
imports: ZArith Basic_type ZnZ Zn2Z Nbasic GenMul GenDivn1