proposition: Lemma DE2_lt0d c d: DE_eq2 c d -> 0 <d.
proof: Proof. rewrite /DE_eq2 =>h;case:(posnP d) => dp //. by move /eqP: h; rewrite dp muln0 addn0 exp0n // addn_eq0 andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)