(*apply (trans_lt ? (S O)).
apply lt_O_S.
assumption*)
| apply (transitive_congruent n ?
(map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
(*apply (trans_lt ? (S O)).
apply lt_O_S.
assumption*)
| apply (transitive_congruent n ?
(map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))