proposition: Lemma bin_int (a b : int) : 0 <= a -> 0 <= b -> exists e : nat, binomialz a b = Posz e.
proof: Proof. by case: a b => [] a [] b //= _ _; rewrite binz_nat_nat; exists 'C(a, b). Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics