Added the following theorems to BinPos:

Pplus_xO
Pmult_Sn_m
Pcompare_eq_Lt (a generalization of Pcompare_Gt_Lt)
Pcompare_eq_Gt (a generalization of Pcompare_Lt_Gt)
Pcompare_refl_id (a generalization of Pcompare_refl)
Pcompare_Lt_eq_Lt (a generalization of Pcompare_Lt_Lt)
Pcompare_Gt_eq_Gt (a generalization of Pcompare_Gt_Gt)
Pcompare_p_Sp
Pcompare_p_Sq (one of the defining axioms of < )
Pcompare_1 (1 is the least positive number)

Added the following theorems to BinNat:
Nrect (defined in terms of new Prect)
Nrect_base
Nrect_step (the analogout statement in BinPos is called Prect_succ)
Nrec_base
Nrec_step
Nmult_Sn_m
Nsucc_0
Ncompare_0 (0 is the least natural number)
Ncompare_n_Sm (one of the defining axioms of < )

Also, defined Nind and Nrec in terms of Nrect.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9738 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions