proposition: Lemma tuto_pred0P : forall P, reflect (P =1 pred0) (pred0b P).
proof: Proof. move=> p; apply: (iffP eqP); [exact: card0_eq | exact: eq_card0]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)