proposition: Lemma cdivides_order : order_r cdivides.
proof: Proof. split. - by move => u v w ha hb; apply: (cdivides_trans hb ha). - move=> u v ha hb. case: (equal_or_not u \0c) => uz. by move: (cdivides_pr ha); rewrite uz cprod0l. case: (equal_or_not v \0c) => vz. by move: (cdivides_pr hb); rewrite vz cprod0l. apply: cleA. exact:(cdivides_smaller ha vz). exact:(cdivides_smaller hb uz). - by move => u v [vN uN _]; split; apply: cdivides_itself. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)