proposition: Lemma tuto_eqVneq : forall x y, {x = y} + {x != y}.
proof: Proof. by move=> x y; case: eqP; [left | right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)