1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/arith/pnat_pred.ma".
16 include "ground/arith/pnat_le.ma".
18 (* ORDER FOR POSITIVE INTEGERS **********************************************)
20 (* Destructions with ppred **************************************************)
22 lemma ple_inv_pred_sn (p) (q): ↓p ≤ q → p ≤ ↑q.
24 /2 width=1 by ple_succ_bi/
27 (* Constructions with ppred *************************************************)
29 lemma ple_succ_pred_dx_refl (p): p ≤ ↑↓p.
30 #p @ple_inv_pred_sn // qed.
32 lemma ple_pred_sn_refl (p): ↓p ≤ p.
36 lemma ple_pred_bi (p) (q): p ≤ q → ↓p ≤ ↓q.
38 /2 width=3 by ple_trans/
41 lemma ple_pred_sn (p) (q): p ≤ ↑q → ↓p ≤ q.
43 /2 width=1 by ple_pred_bi/
46 (* Inversions with ppred ****************************************************)
48 lemma ple_inv_succ_sn (p) (q):
49 ↑p ≤ q → ∧∧ p ≤ ↓q & q = ↑↓q.
51 [ /2 width=3 by ple_refl, conj/
52 | #q #Hq /3 width=1 by ple_des_succ_sn, conj/