proposition: Lemma evenb_plus n m : evenb n -> evenb m -> evenb (n + m).
proof: Proof. elim: n=>[|n Hn]; first by rewrite add0n. Restart. move: (leqnn n). elim: n {-2}n. - by case=>//. move=>n Hn. case=>//. case=>// n0. by move/ltnW /Hn=>//. Qed.
imports: mathcomp(ssreflect eqtype ssrnat ssrbool ssrfun seq)