#p #q #r elim r -r //
#r #IH <pplus_succ_dx <pplus_succ_dx <IH -IH //
qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_unit_pplus (p) (q): 𝟏 = p + q → ⊥.
+#p #q elim q -q
+[ <pplus_one_dx #H destruct
+| #q #_ <pplus_succ_dx #H destruct
+]
+qed-.
+
+lemma eq_inv_pplus_unit (p) (q):
+ p + q = 𝟏 → ⊥.
+/2 width=3 by eq_inv_unit_pplus/ qed-.
+
+lemma eq_inv_pplus_bi_dx (r) (p) (q): p + r = q + r → p = q.
+#r elim r -r /3 width=1 by eq_inv_psucc_bi/
+qed-.
+
+lemma eq_inv_pplus_bi_sn (r) (p) (q): r + p = r + q → p = q.
+#r #p #q <pplus_comm <pplus_comm in ⊢ (???%→?);
+/2 width=2 by eq_inv_pplus_bi_dx/
+qed-.