proposition: Lemma forallb_ext {A} (f g : A -> bool) l : (forall a, f a = g a) -> forallb f l = forallb g l.
proof: Proof. intros e; induction l; simpl; congruence. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)