De las pruebas a los programas.

Welcome to Coq V6.2.2 (September 1998)
Require Export Omega.
[Reinterning Omega ...done]
[Reinterning ZArith ...done]
[Reinterning fast_integer ...done]
[Reinterning Le ...done]
[Reinterning Lt ...done]
[Reinterning Plus ...done]
[Reinterning Mult ...done]
[Reinterning Minus ...done]
[Reinterning zarith_aux ...done]
[Reinterning Arith ...done]
[Reinterning Gt ...done]
[Reinterning Between ...done]
[Loading ML file g_natsyntax.cmo ...done]
[Reinterning auxiliary ...done]
[Reinterning Peano_dec ...done]
[Reinterning Compare_dec ...done]
[Reinterning Zsyntax ...done]
[Loading ML file g_zsyntax.cmo ...done]
[Reinterning ZArith_dec ...done]
[Reinterning Sumbool ...done]
[Reinterning Zmisc ...done]
[Reinterning Bool ...done]
[Reinterning OmegaSyntax ...done]
[Loading ML file omega.cmo ...done]
[Loading ML file coq_omega.cmo ...done]
Require Export Lt.
Warning: Lt already imported
Require Export Compare.
[Reinterning Compare ...done]
[Reinterning Wf_nat ...done]
[Reinterning Min ...done]
Lemma div_euclid: (a,b:nat)
{q:nat*nat| a=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b))}.
1 subgoal
 
  ============================
   (a,b:nat)
    {q:(nat*nat) |
       (a=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Intro a.
1 subgoal
 
  a : nat
  ============================
   (b:nat)
    {q:(nat*nat) |
       (a=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Elim a.
2 subgoals
 
  a : nat
  ============================
   (b:nat)
    {q:(nat*nat) |
       ((0)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (n:nat)
  ((b:nat)
    {q:(nat*nat) |
       (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))})
   ->(b:nat)
      {q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Intros.
2 subgoals
 
  a : nat
  b : nat
  ============================
   {q:(nat*nat) |
      ((0)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (n:nat)
  ((b:nat)
    {q:(nat*nat) |
       (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))})
   ->(b:nat)
      {q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Split with (O,O).
2 subgoals
 
  a : nat
  b : nat
  ============================
   (0)=(plus (Snd ((0),(0))) (mult (Fst ((0),(0))) (S b)))
   /\(lt (Snd ((0),(0))) (S b))

subgoal 2 is:
 (n:nat)
  ((b:nat)
    {q:(nat*nat) |
       (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))})
   ->(b:nat)
      {q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Simpl.
2 subgoals
 
  a : nat
  b : nat
  ============================
   (0)=(0)/\(lt (0) (S b))

subgoal 2 is:
 (n:nat)
  ((b:nat)
    {q:(nat*nat) |
       (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))})
   ->(b:nat)
      {q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Auto.
1 subgoal
 
  a : nat
  ============================
   (n:nat)
    ((b:nat)
      {q:(nat*nat) |
         (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))})
     ->(b:nat)
        {q:(nat*nat) |
           ((S n)=(plus (Snd q) (mult (Fst q) (S b)))
            /\(lt (Snd q) (S b)))}
Intros.
1 subgoal
 
  a : nat
  n : nat
  H : (b:nat)
       {q:(nat*nat) |
          (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
  b : nat
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Elim H with b.
1 subgoal
 
  a : nat
  n : nat
  H : (b:nat)
       {q:(nat*nat) |
          (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
  b : nat
  ============================
   (x:nat*nat)
    n=(plus (Snd x) (mult (Fst x) (S b)))/\(lt (Snd x) (S b))
     ->{q:(nat*nat) |
          ((S n)=(plus (Snd q) (mult (Fst q) (S b)))
           /\(lt (Snd q) (S b)))}
Intros.
1 subgoal
 
  a : nat
  n : nat
  H : (b:nat)
       {q:(nat*nat) |
          (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
  b : nat
  x : nat*nat
  y : n=(plus (Snd x) (mult (Fst x) (S b)))/\(lt (Snd x) (S b))
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
(Elim y; Intros).
1 subgoal
 
  a : nat
  n : nat
  H : (b:nat)
       {q:(nat*nat) |
          (n=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
  b : nat
  x : nat*nat
  y : n=(plus (Snd x) (mult (Fst x) (S b)))/\(lt (Snd x) (S b))
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Clear y H.
1 subgoal
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Elim lt_eq_lt_dec with (S (Snd x)) (S b).
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  ============================
   {(lt (S (Snd x)) (S b))}+{(S (Snd x))=(S b)}
    ->{q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Intro.
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : {(lt (S (Snd x)) (S b))}+{(S (Snd x))=(S b)}
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Elim y.
3 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : {(lt (S (Snd x)) (S b))}+{(S (Snd x))=(S b)}
  ============================
   (lt (S (Snd x)) (S b))
    ->{q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (S (Snd x))=(S b)
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
subgoal 3 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Intros.
3 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : {(lt (S (Snd x)) (S b))}+{(S (Snd x))=(S b)}
  y0 : (lt (S (Snd x)) (S b))
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (S (Snd x))=(S b)
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
subgoal 3 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Clear y.
3 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (lt (S (Snd x)) (S b))
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (S (Snd x))=(S b)
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
subgoal 3 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Split with ((Fst x),(S (Snd x))).
3 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (lt (S (Snd x)) (S b))
  ============================
   (S n)
    =(plus (Snd ((Fst x),(S (Snd x))))
       (mult (Fst ((Fst x),(S (Snd x)))) (S b)))
   /\(lt (Snd ((Fst x),(S (Snd x)))) (S b))

subgoal 2 is:
 (S (Snd x))=(S b)
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
subgoal 3 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Simpl.
3 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (lt (S (Snd x)) (S b))
  ============================
   (S n)=(S (plus (Snd x) (mult (Fst x) (S b))))
   /\(lt (S (Snd x)) (S b))

subgoal 2 is:
 (S (Snd x))=(S b)
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
subgoal 3 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
(Split; Trivial).
3 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (lt (S (Snd x)) (S b))
  ============================
   (S n)=(S (plus (Snd x) (mult (Fst x) (S b))))

subgoal 2 is:
 (S (Snd x))=(S b)
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
subgoal 3 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Omega.
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : {(lt (S (Snd x)) (S b))}+{(S (Snd x))=(S b)}
  ============================
   (S (Snd x))=(S b)
    ->{q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Intros.
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : {(lt (S (Snd x)) (S b))}+{(S (Snd x))=(S b)}
  y0 : (S (Snd x))=(S b)
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Clear y.
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (S (Snd x))=(S b)
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Split with ((S (Fst x)),O).
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (S (Snd x))=(S b)
  ============================
   (S n)
    =(plus (Snd ((S (Fst x)),(0))) (mult (Fst ((S (Fst x)),(0))) (S b)))
   /\(lt (Snd ((S (Fst x)),(0))) (S b))

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Simpl.
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (S (Snd x))=(S b)
  ============================
   (S n)=(S (plus b (mult (Fst x) (S b))))/\(lt (0) (S b))

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Split.
3 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (S (Snd x))=(S b)
  ============================
   (S n)=(S (plus b (mult (Fst x) (S b))))

subgoal 2 is:
 (lt (0) (S b))
subgoal 3 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Omega.
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y0 : (S (Snd x))=(S b)
  ============================
   (lt (0) (S b))

subgoal 2 is:
 (lt (S b) (S (Snd x)))
  ->{q:(nat*nat) |
       ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Auto.
1 subgoal
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  ============================
   (lt (S b) (S (Snd x)))
    ->{q:(nat*nat) |
         ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Intros.
1 subgoal
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : (lt (S b) (S (Snd x)))
  ============================
   {q:(nat*nat) |
      ((S n)=(plus (Snd q) (mult (Fst q) (S b)))/\(lt (Snd q) (S b)))}
Absurd (lt b (Snd x)).
2 subgoals
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : (lt (S b) (S (Snd x)))
  ============================
   ~(lt b (Snd x))

subgoal 2 is:
 (lt b (Snd x))
Omega.
1 subgoal
 
  a : nat
  n : nat
  b : nat
  x : nat*nat
  H0 : n=(plus (Snd x) (mult (Fst x) (S b)))
  H1 : (lt (Snd x) (S b))
  y : (lt (S b) (S (Snd x)))
  ============================
   (lt b (Snd x))
Auto.
Subtree proved!
Defined.
Intro a.
Elim a.
Intros.
Split with (O,O).
Simpl.
Auto.

Intros.
Elim H with b.
Intros.
(Elim y; Intros).
Clear y H.
Elim lt_eq_lt_dec with (S (Snd x)) (S b).
Intro.
Elim y.
Intros.
Clear y.
Split with ((Fst x),(S (Snd x))).
Simpl.
(Split; Trivial).
Omega.

Intros.
Clear y.
Split with ((S (Fst x)),O).
Simpl.
Split.
Omega.

Auto.

Intros.
Absurd (lt b (Snd x)).
Omega.

Auto.

div_euclid is defined
Require Extraction.
[Reinterning Extraction ...done]
[Loading ML file ml_import.cmo ...done]
[Loading ML file mlterm.cmo ...done]
[Loading ML file fw_env.cmo ...done]
[Loading ML file fwtoml.cmo ...done]
[Loading ML file optimise.cmo ...done]
[Loading ML file genpp.cmo ...done]
[Loading ML file caml.cmo ...done]
[Loading ML file haskell.cmo ...done]
[Loading ML file ocaml.cmo ...done]
Extraction div_euclid.
div_euclid ==>
    [a:nat]
     (nat_rec nat->(prod nat nat) [_:nat](pair nat nat O O)
       [_:nat]
        [H:nat->(prod nat nat)]
         [b:nat]
          (sig_rec (prod nat nat) (prod nat nat)
            [x:(prod nat nat)]
             (#GENTERM (CONST #Logic#and_rec.fw) (prod nat nat)
               (sumor_rec sumbool (prod nat nat)
                 [y:sumbool]
                  (sumbool_rec (prod nat nat)
                    (pair nat nat (fst nat nat x) (S (snd nat nat x)))
                    (pair nat nat (S (fst nat nat x)) O) y)
                 (False_rec (prod nat nat))
                 (lt_eq_lt_dec (S (snd nat nat x)) (S b)))) (H b)) a)
 : nat->nat->(prod nat nat)
 

Write Caml File "division" [div_euclid].
The axiom False_rec is translated into an exception.
Warning: The constant nat_rec is expanded.
Warning: The constant fst is expanded.
Warning: The constant snd is expanded.
Warning: The constant and_rec is expanded.
Warning: The constant sig_rec is expanded.
Warning: The constant sumbool_rec is expanded.
Warning: The constant sumor_rec is expanded.
 

Write Haskell File "division" [div_euclid].
The axiom False_rec is translated into an exception.

Los Ficheros extraidos:

OCaml:

type nat =
    O
  | S of nat
;;

type ('a, 'b) prod =
    Pair of 'a * 'b
;;

type sumbool =
    Left_ren
  | Right_ren
;;

type 'a sumor =
    Inleft of 'a
  | Inright
;;

let lt_eq_lt_dec n =
  let rec f1 = function
    O -> (fun m ->
      let rec f3 = function
        O -> Inleft Right_ren
      | S n2 -> Inleft Left_ren
      in f3 m)
  | S n1 -> (fun m ->
      let rec f2 = function
        O -> Inright
      | S n4 ->
          (match f1 n1 n4 with
             Inleft x ->
               (match x with
                  Left_ren -> Inleft Left_ren
                | Right_ren -> Inleft Right_ren)
           | Inright -> Inright)
      in f2 m)
  in f1 n
;;

let div_euclid a =
  let rec f1 = function
    O -> (fun b -> Pair (O, O))
  | S n0 -> (fun b ->
      match lt_eq_lt_dec (S (match f1 n0 b with
                               Pair (x0, y) -> y)) (S b) with
        Inleft x0 ->
          (match x0 with
             Left_ren ->
               Pair ((match f1 n0 b with
                        Pair (x1, y0) -> x1),
                     (S (match f1 n0 b with
                           Pair (x1, y0) -> y0)))
           | Right_ren ->
               Pair ((S (match f1 n0 b with
                           Pair (x1, y0) -> x1)), O))
      | Inright -> failwith "False_rec")
  in f1 a
;;

Haskell:

data Nat = O
         | S Nat

nat_rec f f0 =
  let { f1 n =
    case n of
      O -> f
      S n0 -> f0 n0 (f1 n0) }
  in f1

data Prod a b = Pair a b

fst p =
  case p of
    Pair x y -> x

snd p =
  case p of
    Pair x y -> y

and_rec f =
  f

sig_rec f s =
  f s

data Sumbool = Left_ren
             | Right_ren

sumbool_rec f f0 s =
  case s of
    Left_ren -> f
    Right_ren -> f0

data Sumor a = Inleft a
             | Inright

sumor_rec f f0 s =
  case s of
    Inleft x -> f x
    Inright -> f0

false_rec =
  error "False_rec"

lt_eq_lt_dec n =
  nat_rec
    (\m -> nat_rec (Inleft Right_ren) (\n0 h -> Inleft Left_ren) m)
    (\n0 h m -> nat_rec Inright
                  (\q h' -> sumor_rec
                              (\y -> sumbool_rec (Inleft Left_ren)
                                       (Inleft Right_ren) y) Inright
                              (h q)) m) n

div_euclid a =
  nat_rec (\b -> Pair O O)
    (\n h b -> sig_rec
                 (\x -> and_rec
                          (sumor_rec
                            (\y -> sumbool_rec
                                     (Pair (fst x) (S (snd x)))
                                     (Pair (S (fst x)) O) y) false_rec
                            (lt_eq_lt_dec (S (snd x)) (S b))))
                 (h b)) a