proposition: Lemma cpow_nz a b: a <> \0c -> (a ^c b) <> \0c.
proof: Proof. move=> anz;rewrite - cprod_of_same; apply /cprod_nzP. by hnf; aw => t tb; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)