proposition: Lemma cquo_itself a: natp a -> a <> \0c -> a %/c a = \1c.
proof: Proof. by move=> aN anz; move: (cdivision_itself aN anz) => [ _ h]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)