Library Coq.Arith.Euclid
Require Import Mult.
Require Import Compare_dec.
Require Import Wf_nat.
Open Local 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}.