(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/totient1".
-
include "nat/totient.ma".
include "nat/iteration2.ma".
include "nat/gcd_properties1.ma".
| apply divides_gcd_n
]
]
- | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
+ | apply eq_to_eqb_true.
rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
[ apply (div_n_n (gcd x n) Hcut)
| assumption