proposition: Lemma evenP_contra n : evenP (n + 1 + n) -> False.
proof: Proof. elim: n=>//[| n Hn]; first by rewrite addn0 add0n; case=>//. rewrite addn1 addnS addnC !addnS. rewrite addnC addn1 addnS in Hn. case=>// m /eqP. by rewrite !eqSS; move/eqP=><-. Qed.
imports: mathcomp(ssreflect eqtype ssrnat ssrbool ssrfun seq)