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).