proposition: Lemma tuto_predD1P : forall x y b, reflect (x <> y /\ b) ((x != y) && b).
proof: Proof. by move=> x y b; apply: (iffP andP) => [] []; move/eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)