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