Library Exercise_4_5_1_4


Require Import Utf8.
Require Import OrderProduct Orders NatOrders.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.5.1.4

Section Exercise_4_5_1_4.

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:
(2, 4) (3, 4)? (2, 4) (3, 5)? (2, 4) (8, 0)? (2, 4) (0, 0)?

  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.