proposition: Lemma DE_eq6_alt x y: (DE_eq6 x y) = ((x*+2 - (y+1))^+2 == (y+1)^+2 + (y*+2)^+2).
proof: Proof. rewrite sqrrB mulrnAl -mulrnA !exprMn_n addrC -subr_eq0 [X in _ + X == 0]opprD. rewrite addrACA subrr add0r -mulNrn -mulrnDl -mulNrn -mulrnDl mulrn_eq0 /=. by rewrite mulrDr mulr1 opprD !addrA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)