proposition: Lemma DE2_pos c d: 0 < c -> DE_eq2 c d -> d <= c < d.*2.
proof: Proof. move => ha hb. move: (leq_mul ha (DE2_lt0d hb)); rewrite -(leq_add2l (d^2)) - hb. rewrite leq_add2r leq_exp2r // => -> /=. case: (ltnP c d.*2) => // hc. have ea: 4 * d^2 <= c^2 by rewrite -[4]/(2^2) -(expnMn 2) mul2n leq_exp2r. have eb: 4 * (c * d) <= 2 * c^2. by rewrite -[4]/(2*2) mulnACA (mul2n d) -mulnn mulnA leq_mul2l hc orbT. move: (leq_add ea eb); rewrite -mulnDr -hb mulnDr -mulSn mulSnr. by rewrite -[X in _ <= X](addn0) -addnA leq_add2l addnS ltn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)