proposition: Lemma cquo_zero a: a %/c \0c = \0c.
proof: Proof. rewrite cquoE /cquo_internal /least_ordinal; set E := Zo _ _. have -> : E = emptyset. apply /set0_P => y /Zo_hi; rewrite cprod0l; apply: clt0. by rewrite setI_0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)