proposition: Fact lt_0_c (i j : int) : 0 <= j <= i -> 0 < c i j.
proof: Proof. case/andP=> h0j hji; rewrite /c -expfzMl. by apply/exprz_gt0/mulr_gt0; rewrite ltr0z binz_gt0; lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics binomialz seq_defs