proposition: Lemma nds_sc_exten X X' n f: natp n -> (same_below X X' n) -> inc f (permutations n) -> nds_sc X n f = nds_sc X' n f.
proof: Proof. move => nN h /Zo_P [ /functionsP [fg sg tg] bg ];apply: (osumf_exten nN). move => i /(NltP nN) ia; apply: h; apply/(NltP nN); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)