# Library Exercise_4_5_1_4

Require Import Utf8.

Require Import OrderProduct Orders NatOrders.

Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.

## Problem

Consider the partial order ≤ on ℕ given by standard "less-than-or-equal-to", so 5 ≤ 9 etc. And consider another partial order, divides on ℕ, where a divides b if "a goes into b evenly", i.e. if there exists n : ℕ such that a × n = b, so 5 divides 35. If we call the product order (X, ≼) := (ℕ, ≤) × (ℕ, divides), which of the following are true:Local Infix "≤" := le.

Local Infix "≼" := (fun n m ⇒ @dec_rel _ (le × divides)%relation _ n m) (at level 70, right associativity).

Eval hnf in (2, 4) ≼ (3, 4).

Eval hnf in (2, 4) ≼ (3, 5).

Eval hnf in (2, 4) ≼ (8, 0).

Eval hnf in (2, 4) ≼ (0, 0).

End Exercise_4_5_1_4.