proposition: Lemma DE_equiv_56 x y: (DE_eq5 x y) = (DE_eq6 (-x) y).
proof: Proof. by rewrite /DE_eq5 /DE_eq6 sqrrN opprK mulNr opprK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)