# 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 }.