proposition: Lemma zpartial_sum_mon_bis c n m: znat_fam c -> intp n -> intp m -> zpartial_sum c n <z zpartial_sum c m -> n <z m.
proof: Proof. move => ha nz mz le. by case: (zleT_el mz nz) => // /(zpartial_sum_mon ha) /zleNgt; case. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)