proposition: Lemma DE2_rec' c d: 0 < c -> DE_eq2 c d -> DE_eq2 (c-d) (d.*2-c).
proof: Proof. move => cp h. move /andP:(DE2_pos cp h) => [ea eb];apply/DE2_rec. have xv:=(subnK ea). move/eqP: (subnK (ltnW eb)); rewrite -addnn - {2}xv addnA eqn_add2r addnC. by rewrite -addnn -addnA;move/eqP ->; rewrite xv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)