+(* Basic inversions ********************************************************)
+
+lemma pcc_inv_empty (n):
+ (๐) ฯต ๐โจnโฉ โ ๐ = n.
+#n @(insert_eq_1 โฆ (๐))
+#x * -n //
+#p #n [ #k ] #_ #H0 destruct
+qed-.
+
+lemma pcc_inv_d_dx (p) (n) (k):
+ pโ๐ฑk ฯต ๐โจnโฉ โ p ฯต ๐โจn+kโฉ.
+#p #n #h @(insert_eq_1 โฆ (pโ๐ฑh))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+lemma pcc_inv_m_dx (p) (n):
+ pโ๐บ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
+#p #n @(insert_eq_1 โฆ (pโ๐บ))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+lemma pcc_inv_L_dx (p) (n):
+ pโ๐ ฯต ๐โจnโฉ โ
+ โงโง p ฯต ๐โจโnโฉ & โโn = n.
+#p #n @(insert_eq_1 โฆ (pโ๐))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct
+<npred_succ /2 width=1 by conj/
+qed-.
+
+lemma pcc_inv_A_dx (p) (n):
+ pโ๐ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
+#p #n @(insert_eq_1 โฆ (pโ๐))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+lemma pcc_inv_S_dx (p) (n):
+ pโ๐ฆ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
+#p #n @(insert_eq_1 โฆ (pโ๐ฆ))
+#x * -x -n
+[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+qed-.
+
+(* Advanced inversions ******************************************************)
+
+lemma pcc_inv_empty_succ (n):
+ (๐) ฯต ๐โจโnโฉ โ โฅ.
+#n #H0
+lapply (pcc_inv_empty โฆ H0) -H0 #H0
+/2 width=7 by eq_inv_zero_nsucc/
+qed-.
+
+lemma pcc_inv_L_dx_zero (p):
+ pโ๐ ฯต ๐โจ๐โฉ โ โฅ.
+#p #H0
+elim (pcc_inv_L_dx โฆ H0) -H0 #_ #H0
+/2 width=7 by eq_inv_nsucc_zero/
+qed-.