proposition: Lemma tuto_andP : forall b1 b2 : bool, reflect (b1 /\ b2) (b1 && b2).
proof: Proof. by case; case; constructor; auto; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)