proposition: Lemma involutiveP (A : finType) (f : {ffun A -> A}) : reflect (involutive f) (involutiveb f).
proof: Proof. by apply: (iffP forallP) => [H x|H x]; [rewrite (eqP (H x)) | rewrite H]. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple