proposition: Lemma LS_nextP_pr5 X P E: sub P X -> finite_set E -> sub E (LS_res X P) -> exists2 m, natp m & sub E (Vf (LS_rec X P) m).
proof: Proof. move => pa; move: E; apply: finite_set_induction. move => _; exists \0c; fprops. move => a b Hrec h1. have [m mN mv]:= (Hrec(sub_trans (@sub_setU1 a b) h1)). move: (h1 _ (setU1_1 a b)) => /LS_res_p0 [n nN nv]. move: (NS_sum nN mN)(Nsum_M0le n mN) (Nsum_M0le m nN); rewrite (csumC m). set k := n +c m => ra rb rc; exists k => //. move => t /setU1_P; case; first by move => /mv; apply:(LS_nextP_pr4 pa rb ra). move => ->; apply:(LS_nextP_pr4 pa rc ra nv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)