proposition: Lemma binom1 n: natp n -> binom n \1c = n.
proof: Proof. move: n; rewrite - succ_zero;apply: Nat_induction. rewrite binom0Sm; fprops. move=> p pN r. by rewrite (binomSnSm pN NS0) r (binom0 pN) (Nsucc_rw pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)