(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/dirichlet_product".
-
include "nat/primes.ma".
include "Z/sigma_p.ma".
include "Z/times.ma".
assumption
]
|elim (divides_b_true_to_divides ? ? H4).
- apply (witness ? ? n2).
+ apply (witness ? ? n1).
rewrite > assoc_times.
rewrite < H5.
rewrite < sym_times.