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.