Xavier.v

Section Gcd. 

  Fixpoint gcd_rec (a b : nat) (acc : Acc lt b) {struct acc} : nat :=
    match Nat.eq_dec b 0 with 
    | left _ => a 
    | right Ha => gcd_rec b (Nat.modulo a b) 
      (Acc_inv acc (Nat.mod_upper_bound a b Ha))
    end.
    
  Definition gcd (a b : nat) : nat.
  refine 
    match b <=? a with 
    | true => gcd_rec a b (lt_wf b) 
    | _ => gcd_rec b a (lt_wf a)
    end. 
  Defined. 

  Eval compute in gcd 1 2. 
End Gcd.