Library Coq.NArith.Pnat
Properties of the injection from binary positive numbers to Peano
natural numbers
Original development by Pierre Crégut, CNET, Lannion, France
Require Import Le.
Require Import Lt.
Require Import Gt.
Require Import Plus.
Require Import Mult.
Require Import Minus.
Require Import Compare_dec.
Local Open Scope positive_scope.
Local Open Scope nat_scope.
nat_of_P is a morphism for addition
Pmult_nat is a morphism for addition
nat_of_P is a morphism for multiplication
nat_of_P maps to the strictly positive subset of nat
Extra lemmas on lt on Peano natural numbers
Lemma ZL7 :
forall n m:
nat,
n < m ->
n + n < m + m.
Lemma ZL8 :
forall n m:
nat,
n < m ->
S (
n + n)
< m + m.
nat_of_P is a morphism from positive to nat for lt (expressed
from compare on positive)
Part 1: lt on positive is finer than lt on nat
nat_of_P is a morphism from positive to nat for gt (expressed
from compare on positive)
Part 1: gt on positive is finer than gt on nat
nat_of_P is a morphism for Pcompare and nat_compare
nat_of_P is hence injective.
nat_of_P is a morphism from positive to nat for lt (expressed
from compare on positive)
Part 2: lt on nat is finer than lt on positive
nat_of_P is a morphism from positive to nat for gt (expressed
from compare on positive)
Part 2: gt on nat is finer than gt on positive
nat_of_P is strictly positive
Pmult_nat permutes with multiplication
Mapping of xH, xO and xI through nat_of_P
Properties of the shifted injection from Peano natural numbers to
binary positive numbers
Composition of P_of_succ_nat and nat_of_P is successor on nat
Miscellaneous lemmas on P_of_succ_nat
Composition of nat_of_P and P_of_succ_nat is successor on positive
Composition of nat_of_P, P_of_succ_nat and Ppred is identity
on positive
Extra properties of the injection from binary positive numbers to Peano
natural numbers
nat_of_P is a morphism for subtraction on positive numbers
Comparison and subtraction
Distributivity of multiplication over subtraction