proposition: Lemma nds_sums_exten Y1 Y2 m: natp m -> same_below Y1 Y2 m -> nds_sums Y1 m = nds_sums Y2 m.
proof: Proof. move => ha hb;set_extens t; move => /funI_P [z zp ->];apply/funI_P; ex_tac. by apply:nds_sc_exten. by symmetry;apply:nds_sc_exten. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)