proposition: Lemma LS_nextP_pr3 X P (Y:= LS_res X P): sub P X -> sub P Y /\ sub Y X.
proof: Proof. move => h; split. move => t tP; move:(proj1 (LS_nextP_pr2 h NS0) _ tP) => h1. apply/LS_res_p0; exists \0c; [exact NS0 | exact]. move => y /LS_res_p0 [n nN ha]; apply: (proj2 (LS_nextP_pr2 h nN) _ ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)