Library Coq.Arith.Euclid

Require Import PeanoNat.
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}.