proposition: Lemma DE2_rec c d: DE_eq2 c d <-> DE_eq2 (c.*2 +d) (c+d).
proof: Proof. rewrite /DE_eq2 -{1}addnn -addnA (addnC c) sqrnD -addnA -addnA (addnC(_ * _) 1). rewrite (addnA (c^2)) mul2n doubleMr (addnC (_ + 1)) (mulnC _ c.*2) addnA. rewrite mulnDl (addnA ((c + d) ^ 2)) (addnC (d^2)) mulnC - mulnn -mulnDr. by split; [ move => -> | move/eqP; rewrite eqn_add2l => /eqP]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)