proposition: Lemma cquo_small a b: natp b -> a <c b -> a %/c b = \0c.
proof: Proof. move => bN lab. have aN:=(NS_lt_nat lab bN). have h: cdivision_prop a b \0c a. by split => //; rewrite cprod0r (csum0l (CS_nat aN)). symmetry; exact:(proj1 (cquorem_pr aN bN NS0 aN h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)