proposition: Lemma binz_Znat_gt0 (n k : int) : n \is a Znat -> k \is a Znat -> k <= n -> 0 < binomialz n k.
proof: Proof. by move=> /ZnatP[{}n ->] /ZnatP[{}k ->] le_kn; rewrite binz_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics