proposition: Lemma evenP_plus n m : evenP n -> evenP m -> evenP (n + m).
proof: Proof. elim=>//n'; first by move=>->; rewrite add0n. move=> m'->{n'} H1 H2 H3; rewrite addnC !addnS addnC. Check EvenSS. apply: (EvenSS _ (m' + m))=>//. by apply: H2. Qed.
imports: mathcomp(ssreflect eqtype ssrnat ssrbool ssrfun seq)