]>
matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/Z/dirichlet_product.ma
[apply sym_eq.
apply div_plus_times.
assumption
[apply sym_eq.
apply div_plus_times.
assumption
]
|apply lt_mod_m_m.
assumption
]
|apply lt_mod_m_m.
assumption