theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
intros.
theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
intros.