proposition: Lemma PS_incr_n_simplify (a : nat -> V) (n k : nat) : PS_incr_n a n k = match (le_lt_dec n k) with | left _ => a (k-n)%nat | right _ => zero end.
proof: Proof. case: le_lt_dec => H. elim: n k H => [ | n IH] k H. rewrite /PS_incr_n ; by case: k H. case: k H => [ | k] H. by apply Nat.nle_succ_0 in H. rewrite /PS_incr_n -/PS_incr_n /PS_incr_1. rewrite IH. apply f_equal. by elim: n k H {IH} => /= [ | n IH] k H. by apply le_S_n. elim: n k H => [ | n IH] k H. by apply Nat.nlt_0_r in H. rewrite /PS_incr_n -/PS_incr_n /PS_incr_1. case: k H => [ | k] H. by []. by apply IH, Nat.succ_lt_mono. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series