proposition: Lemma nds_merge_prop2 k X n: natp k -> natp n -> opos_below X n -> (forall i, i <c k -> odegree (nds_merge k X i) = \1c) /\ (forall i, k <=c i -> i <c (k +c n) -> \1c <o (odegree (nds_merge k X i))).
proof: Proof. move => kN nN hX; rewrite /nds_merge; split. move => i lik; Ytac0;exact:(proj31 (nds_base_prop (NS_lt_nat lik kN))) => dx. move => i lik lin. move:(NS_lt_nat lin (NS_sum kN nN)) => 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. move: (hX _ lt2) => xp. rewrite (odegree_prod (oopow_pos OS2) xp) (odegree_opow OS2). apply:(olt_leT olt_12); apply: (osum_Mle0 OS2 (OS_degree (proj32_1 xp))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)