proposition: Lemma osum_shift n X: natp n -> nds_ax X n -> ordinalp (osumf X n) /\ osumf (fun i => (nds_shift (X i))) n = nds_shift (osumf X n).
proof: Proof. move:n; apply: Nat_induction. rewrite !osum_f0 /nds_shift oprod0r; split; fprops. move => n nN Hrec /(true_below_rec nN) [/Hrec [qa qb] ov]. rewrite !(osum_fS _ nN); split; first by apply: (OS_sum2 ov qa). by rewrite qb /nds_shift (oprodD ov qa (OS_oopow OS2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)