proposition: Lemma modnS x1 x2 : (x1 == x2 %[mod 2]) = (x1.+1 == x2.+1 %[mod 2]).
proof: Proof. by rewrite -![_.+1 as X in X %% 2]add1n eqn_modDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep