N

About N

We prove some basic lemmas of the natural numbers.

A variant of 0_S from the standard library

Lemma S_O : forall n : N, S n <> 0.

Apartness

Definition ap_nat (x y : N) := ~ (x = y :>nat).

Infix "{#N}" := ap_nat (no associativity, at level 90).

Lemma ap_nat_irreflexive0 : forall x : N, ~ (x{#N}x).

Lemma ap_nat_symmetric0 : forall x y : N, (x{#N}y) -> y{#N}x.

Lemma ap_nat_cotransitive0 : forall x y : N,
(x{#N}y) -> forall z : N, (x{#N}z) or (z{#N}y).

Lemma ap_nat_tight0 : forall x y : N, ~ (x{#N}y) <-> x = y.

Addition

Lemma plus_strext0 : forall x1 x2 y1 y2 : N,
(x1+y1{#N}x2+y2) -> (x1{#N}x2) or (y1{#N}y2).

There is no inverse for addition, because every candidate will fail for 2

Lemma no_inverse0 : forall f : N -> N, ~ ((2+f 2) = 0 /\ (f 2+2) = 0).

Multiplication

Lemma mult_strext0 : forall x1 x2 y1 y2 : N,
(x1*y1{#N}x2*y2) -> (x1{#N}x2) or (y1{#N}y2).

Decidability

Lemma not_or:(forall (p q:nat), (p<>q)-> p<q or q<p):CProp.