fact: Definition binom n m := Vg (induction_term (fun _ T: Set => Lg Nat (fun z => variant \0c \1c (Vg T z +c Vg T (cpred z)) z)) (Lg Nat (variant \0c \1c \0c)) n) m.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)