proposition: Lemma nds_merge_prop1 k X n: natp k -> natp n -> opos_below X n -> opos_below (nds_merge k X) (k +c n).
proof: Proof. move => kN nN hX i lin. rewrite/nds_merge. move:(NS_lt_nat lin (NS_sum kN nN)) => iN. case:(NleT_el kN iN) => lik; last by Ytac0; exact:(proj1 (nds_small_base iN)). rewrite (Y_false (cleNgt lik)). move: (cdiff_pr lik) => iv. have lt2: i -c k <c n by apply:(csum_lt2l kN (NS_diff k iN) nN); ue. apply: (oprod2_pos (oopow_pos OS2) (hX _ lt2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)