proposition: Lemma LS_nextP_pr4 X P n m: sub P X -> n <=c m -> inc m Nat -> sub (Vf (LS_rec X P) n) (Vf (LS_rec X P) m).
proof: Proof. move => h0 nm mN. move:(NS_le_nat nm mN) => nN. move:(NS_diff n mN);rewrite -{2} (cdiff_pr nm); move:(m -c n). apply: Nat_induction; first by rewrite (csum0r (proj31 nm)). move:(induction_defined_pr (LS_nextP X) P). rewrite -/(LS_rec _ _); move => [h1 h2 h3 h4]. move => p pN hrec; rewrite (csum_nS _ pN) h4; fprops. have hr1:= (proj2 (LS_nextP_pr2 h0 (NS_sum nN pN))). by apply: (sub_trans hrec); apply: LS_nextP_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)