Theorem  div_euclid:forall (a b:nat) ,                                                       
       {q:(nat*nat) |  a=(fst q)*(S b)+(snd q) /\ (snd q) < (S  b)}.
Proof.
induction a.
exists (0,0);simpl;auto.
split;auto.

Require Export Arith.
apply lt_O_Sn.

intro.

elim (IHa b);intros.

Check lt_eq_lt_dec .
elim  lt_eq_lt_dec with (S (snd x)) (S b).
intros.
destruct a0.
exists ((fst x), (S (snd x))).
simpl.
Require Export Omega.
omega.

exists ((S (fst x)),0).
simpl;omega.
intros.
absurd (S b < S (snd x));auto.
omega.
Qed.



Extraction "/home/freire/md2/c08-09/div" div_euclid.

Lemma no_cero_S:forall b, (b<>0)-> {n:nat | b = S n}.
Check O_or_S.
intros.
destruct (O_or_S b).
elim s;intros.
exists ( x).
auto.
rewrite e in H.
intuition.
Qed.


Theorem  div_euclid_c:forall (a b:nat) ,    (b<>0)->                                                   
       {q:(nat*nat) |  a=(fst q)* b+(snd q) /\ (snd q) <  b}.
intros.
cut ({n:nat | b= S n}).
2:apply no_cero_S.
2:auto.

intros.
elim H0;intros.
rewrite p.
apply
 div_euclid.
Qed.

Recursive Extraction div_euclid.