proposition: Lemma cdiff_pr7 a b c: a <=c b -> b <c c -> natp c -> (b -c a) <c (c -c a).
proof: Proof. move => le1 lt2 cN. have bN:= (NS_lt_nat lt2 cN). have aN:= (NS_le_nat le1 bN). move:(NS_diff a bN) (NS_diff b cN) => ha hb. rewrite -(cdiff_pr (proj1 lt2)) - {2}(cdiff_pr le1) - csumA csumC. rewrite (cdiff_pr1 (NS_sum ha hb) aN);apply: (csum_M0lt ha (cdiff_nz lt2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)