Library Coq.Arith.Euclid
Require
Import
Mult
.
Require
Import
Compare_dec
.
Require
Import
Wf_nat
.
Local Open
Scope
nat_scope
.
Implicit
Types
a
b
n
q
r
:
nat
.
Inductive
diveucl
a
b
:
Set
:=
divex
:
forall
q
r
,
b
>
r
->
a
=
q
*
b
+
r
->
diveucl
a
b
.
Lemma
eucl_dev
:
forall
n
,
n
>
0
->
forall
m
:
nat
,
diveucl
m
n
.
Lemma
quotient
:
forall
n
,
n
>
0
->
forall
m
:
nat
,
{
q
:
nat
|
exists
r
:
nat
,
m
=
q
*
n
+
r
/\
n
>
r
}
.
Lemma
modulo
:
forall
n
,
n
>
0
->
forall
m
:
nat
,
{
r
:
nat
|
exists
q
:
nat
,
m
=
q
*
n
+
r
/\
n
>
r
}
.