proposition: Lemma edivn2P n : edivn_spec n 2 (edivn2 0 n).
proof: Proof. rewrite -[n]odd_double_half addnC -{1}[n./2]addn0 -{1}mul2n mulnC. elim: n./2 {1 4}0 => [|r IHr] q; first by case (odd n) => /=. by rewrite addSnnS; apply: IHr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)