summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
99431d7)
fermat_little_theorem. It does no longer, but the old behaviour seems to be
really lucky. Thus I change the .ma file.
[rewrite > Hcut3.apply congruent_n_n
|rewrite < eq_map_iter_i_pi.
rewrite < eq_map_iter_i_pi.
[rewrite > Hcut3.apply congruent_n_n
|rewrite < eq_map_iter_i_pi.
rewrite < eq_map_iter_i_pi.
- apply permut_to_eq_map_iter_i
+ apply (permut_to_eq_map_iter_i ? ? ? ? ? (λm.m))
[apply assoc_times
|apply sym_times
|rewrite < plus_n_Sm.
[apply assoc_times
|apply sym_times
|rewrite < plus_n_Sm.