tex
  title = "Euclidian division"
  author = "Christophe Raffalli"
  institute = "\\'Equipe de logique de Paris VII (URA 753)"
  documents = math
.



Import nat.

(* starts automatic detection of axioms *)
flag auto_lvl 1.

goal /\p,d : N (d != N0 -> \/q,r:N (r < d & p = q * d + r)). 
(*! math
\begin{theorem}
$$\[[ $0 \]]$$
\end{theorem}
\begin{proof}
*)
intros.
(*! math
Let us choose $\[ p \] , \[ d \]$ two natural numbers with $\[ $$H1 \]$. 
We prove the following by induction on p: $\[ $0 \]$.
*)
elim -4 H well_founded.N.
intros.
(*! math
Let us choose $\[ a \]$ a strictly positive natural.
We assume $$\[ $$ H3 \]$$ and we must prove $\[ $0 \]$.
*)
elim  -1 d -3 a lesseq.case1.N.
next.
(*! math
We distinguish two cases: $\[ $$H4 \]$ and $\[1 $$H4 \]$.
*)
intros $\/ $&.
next -3.
instance ?1 N0.
instance ?2 a.
(*! math
In the first case, we choose $\[ q = ?1 \]$ and $\[ r = ?2 \]$.
*)
intro.
trivial.
local a' = a - d.
(*! math 
In the second case, we take $\[ a' = $$a' \]$.
*)
elim -1 a' H3.
trivial.
elim lesseq.S_rsub.N.
elim -1 [case] H0.
trivial =H1 H5.
trivial.
lefts H5 $& $\/.
(*! math 
Using the induction hypothesis on $\[ a' \]$, we find two naturals
$\[ q \] , \[ r \]$ such that $\[ $$H7 \]$ and $\[ $$H8 \]$.
*)
intros $& $\/.
next -3.
instance ?4 r.
instance ?3 S q.
(*! math
We choose $\[ ?3 \]$ and $\[ ?4 \]$ as quotient and remaining
for the division of $\[ a \]$. We must prove $\[ $0 \]$ which is immediate.
*)
rewrite mul.lS.N -r add.associative.N -r H8.
intro.
trivial.
(*! math
\qed\end{proof}
*)
save euclide_exists.