Library hilbert.euclid

Require Import Arith.

Require Import Euclid.
Check diveucl.

About quotient.

Definition quo (n:nat)(H:0<n)(p:nat): nat :=
  match quotient n H p with exist q _ => q end.

Check (forall n (H:n>0), quo n H n =1).

Implicit Arguments quo.

Check (forall n (H:n>0), quo H n =1).

Require Import Epsilon.

Definition quo' n p := iota 0 (fun q => 0 < n /\
                                           exists r, n = q * p + r /\ p > r).