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