latte-integers.divides

The divisibility relation defined on ℤ.

(divides [m int] [n int])

(exists [p int] (= (* m p) n))

Definition: The divisibility relation. (divides m n) says that m divides n.

(divides-nat-antisym [m int] [n int])

(==> (elem m nat) (elem n nat) (divides m n) (divides n m) (= m n))

Theorem: Antisymmetry of divisibility only applies to naturals.

(divides-one [n int])

(divides one n)

Theorem:

(divides-opp [m int] [n int])

(==> (divides m n) (divides (-- m) n))

Theorem:

(divides-refl [n int])

(divides n n)

Theorem:

(divides-trans [m int] [n int] [p int])

(==> (divides m n) (divides n p) (divides m p))

Theorem:

(divides-zero [n int])

(divides n zero)

Theorem:

(divides-zero-conv [n int])

(==> (divides zero n) (= n zero))

Theorem:

(divides-zero-zero)

(divides zero zero)

Theorem:

Generated by Codox