proposition: Lemma cdivides_oner x: x %|c \1c -> x = \1c.
proof: Proof. move => xp;move/cdivides_pr: (xp) => /esym p1. by case:(cprod_eq1 (CS_nat (proj32 xp)) (CS_nat (NS_quo x NS1)) p1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)