qed.
theorem nplus_shift_succ_sx: \forall p,q,r.
(p + (succ q) == r) \to (succ p) + q == r.
intros.
lapply linear nplus_gen_succ_2 to H as H0.
qed.
theorem nplus_shift_succ_sx: \forall p,q,r.
(p + (succ q) == r) \to (succ p) + q == r.
intros.
lapply linear nplus_gen_succ_2 to H as H0.
qed.
theorem nplus_shift_succ_dx: \forall p,q,r.
((succ p) + q == r) \to p + (succ q) == r.
intros.
lapply linear nplus_gen_succ_1 to H as H0.
qed.
theorem nplus_shift_succ_dx: \forall p,q,r.
((succ p) + q == r) \to p + (succ q) == r.
intros.
lapply linear nplus_gen_succ_1 to H as H0.