`data Factor : Nat -> Nat -> Type`

Factor n p is a witness that p is indeed a factor of n,

i.e. there exists a q such that p * q = n.

**Totality**: total

**Visibility**: public export

**Constructor**:`CofactorExists : (q : Nat) -> n = p * q -> Factor p n`

**Hints**:`data NotFactor : Nat -> Nat -> Type`

NotFactor n p is a witness that p is NOT a factor of n,

i.e. there exist a q and an r, greater than 0 but smaller than p,

such that p * q + r = n.

**Totality**: total

**Visibility**: public export

**Constructors**:`ZeroNotFactorS : (n : Nat) -> NotFactor 0 (S n)`

`ProperRemExists : (q : Nat) -> (r : Fin (pred p)) -> n = (p * q) + S (finToNat r) -> NotFactor p n`

`data DecFactor : Nat -> Nat -> Type`

DecFactor n p is a result of the process which decides

whether or not p is a factor on n.

**Totality**: total

**Visibility**: public export

**Constructors**:`ItIsFactor : Factor p n -> DecFactor p n`

`ItIsNotFactor : NotFactor p n -> DecFactor p n`

`data CommonFactor : Nat -> Nat -> Nat -> Type`

CommonFactor n m p is a witness that p is a factor of both n and m.

**Totality**: total

**Visibility**: public export

**Constructor**:`CommonFactorExists : (p : Nat) -> Factor p a -> Factor p b -> CommonFactor p a b`

**Hint**:`Symmetric Nat (CommonFactor p)`

`data GCD : Nat -> Nat -> Nat -> Type`

GCD n m p is a witness that p is THE greatest common factor of both n and m.

The second argument to the constructor is a function which for all q being

a factor of both n and m, proves that q is a factor of p.

This is equivalent to a more straightforward definition, stating that for

all q being a factor of both n and m, q is less than or equal to p, but more

powerful and therefore more useful for further proofs. See below for a proof

that if q is a factor of p then q must be less than or equal to p.

**Totality**: total

**Visibility**: public export

**Constructor**:`MkGCD : NotBothZero a b => Lazy (CommonFactor p a b) -> ((q : Nat) -> CommonFactor q a b -> Factor q p) -> GCD p a b`

**Hint**:`Symmetric Nat (GCD p)`

`cofactor : Factor p n -> (q : Nat ** Factor q n)`

Given a statement that p is factor of n, return its cofactor.

**Totality**: total

**Visibility**: export`oneIsFactor : (n : Nat) -> Factor 1 n`

1 is a factor of any natural number.

**Totality**: total

**Visibility**: export`oneSoleFactorOfOne : (a : Nat) -> Factor a 1 -> a = 1`

1 is the only factor of itself

**Totality**: total

**Visibility**: export`factorNotFactorAbsurd : Factor p n -> Not (NotFactor p n)`

No number can simultaneously be and not be a factor of another number.

**Totality**: total

**Visibility**: export`anythingFactorZero : (a : Nat) -> Factor a 0`

Anything is a factor of 0.

**Totality**: total

**Visibility**: export`multFactor : (p : Nat) -> (q : Nat) -> Factor p (p * q)`

For all natural numbers p and q, p is a factor of (p * q).

**Totality**: total

**Visibility**: export`factorLteNumber : Factor p n -> LTE 1 n => LTE p n`

If n > 0 then any factor of n must be less than or equal to n.

**Totality**: total

**Visibility**: export`plusDivisorAlsoFactor : Factor p n -> Factor p (n + p)`

If p is a factor of n, then it is also a factor of (n + p).

**Totality**: total

**Visibility**: export`plusDivisorNeitherFactor : NotFactor p n -> NotFactor p (n + p)`

If p is NOT a factor of n, then it also is NOT a factor of (n + p).

**Totality**: total

**Visibility**: export`multNAlsoFactor : Factor p n -> (a : Nat) -> LTE 1 a => Factor p (n * a)`

If p is a factor of n, then it is also a factor of any multiply of n.

**Totality**: total

**Visibility**: export`plusFactor : Factor p n -> Factor p m -> Factor p (n + m)`

If p is a factor of both n and m, then it is also a factor of their sum.

**Totality**: total

**Visibility**: export`minusFactor : Factor p (a + b) -> Factor p a -> Factor p b`

If p is a factor of a sum (n + m) and a factor of n, then it is also

a factor of m. This could be expressed more naturally with minus, but

it would be more difficult to prove, since minus lacks certain properties

that one would expect from decent subtraction.

**Totality**: total

**Visibility**: export`modFactorAlsoFactorOfDivider : {auto 0 nNotZ : NonZero n} -> Factor p n -> Factor p (modNatNZ m n nNotZ) -> Factor p m`

If p is a common factor of n and mod m n, then it is also a factor of m.

**Totality**: total

**Visibility**: export`commonFactorAlsoFactorOfMod : {auto 0 nNotZ : NonZero n} -> Factor p m -> Factor p n -> Factor p (modNatNZ m n nNotZ)`

If p is a common factor of m and n, then it is also a factor of their mod.

**Totality**: total

**Visibility**: export`decFactor : (n : Nat) -> (d : Nat) -> DecFactor d n`

A decision procedure for whether of not p is a factor of n.

**Totality**: total

**Visibility**: export`factNotSuccFact : GT p 1 -> Factor p n -> NotFactor p (S n)`

For all p greater than 1, if p is a factor of n, then it is NOT a factor

of (n + 1).

**Totality**: total

**Visibility**: export`commonFactorAlsoFactorOfGCD : Factor p a -> Factor p b -> GCD q a b -> Factor p q`

If p is a common factor of a and b, then it is also a factor of their GCD.

This actually follows directly from the definition of GCD.

**Totality**: total

**Visibility**: export`oneCommonFactor : (a : Nat) -> (b : Nat) -> CommonFactor 1 a b`

1 is a common factor of any pair of natural numbers.

**Totality**: total

**Visibility**: export`selfIsCommonFactor : (a : Nat) -> LTE 1 a => CommonFactor a a a`

Any natural number is a common factor of itself and itself.

**Totality**: total

**Visibility**: export`gcd : (a : Nat) -> (b : Nat) -> NotBothZero a b => (f : Nat ** GCD f a b)`

An implementation of Euclidean Algorithm for computing greatest common

divisors. It is proven correct and total; returns a proof that computed

number actually IS the GCD.

**Totality**: total

**Visibility**: export`gcdUnique : GCD p a b -> GCD q a b -> p = q`

For every two natural numbers there is a unique greatest common divisor.

**Totality**: total

**Visibility**: export`divByGcdGcdOne : GCD a (a * b) (a * c) -> GCD 1 b c`

For every two natural numbers, if we divide both of them by their GCD,

the GCD of resulting numbers will always be 1.

**Totality**: total

**Visibility**: export