proposition: Lemma nds_card_exten Y1 Y2 m: natp m -> same_below Y1 Y2 m -> nds_card Y1 m = nds_card Y2 m.
proof: Proof. by move => ha hb; rewrite /nds_card (nds_sums_exten ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)