NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library div_ext

Require Import ssreflect div ssrnat ssrbool.
Export div.

Lemma dvdn_0 : forall n, n <> 0 -> ~ 0 %| n.

Lemma divn_lt0 : forall a b, 0 < a -> 0 < a %/ (gcdn a b).