comomn tatics

1377 apply
1154 auto
1024 rewrite
 994 destruct
 867 intros
 574 omega
 539 assert
 472 intro
 440 simpl
 345 unfold
 328 exists
 281 replace
 259 induction
 147 end
 145 split
 135 match
 125 case
 121 forall
 100 ring
 100 elim
  96 clear
  89 inversion
  81 generalize
  77 left
  72 right
  66 specialize
  64 exact
  60 reflexivity
  49 remember
  49 assumption
  44 repeat
  43 tauto
  43 pow
  40 trivial
  39 cut
  34 contradict
  33 absurd
  31 ring_simplify
  31 if
  28 cbv
  27 symmetry
  27 pose
  26 nat
  24 set
  24 discriminate
  23 fold
  23 congruence
  23 cardauto
  22 contradiction
  20 compute
  19 card
  18 try
  18 change
  17 revert
  17 eapply
  17 do
  16 erewrite
  15 sum
  14 height
  13 constructor
  12 omega]
  11 intuition
  11 edestruct
  10 transitivity
  10 rwc
  10 injective
  10 f_equal
   9 let
   8 rel_prime
   8 injection
   8 else
   8 case_eq
   7 xs
   7 with
   7 unionl
   7 pattern
   7 even
   7 eq
   6 set_eq
   6 prove_sup
   6 prime
   6 nil
   6 id_after_false
   6 finite_sub
   6 elimtype
   5 x^
   5 vm_compute
   5 subst
   5 red
   5 nat_rec
   5 lt_true_upto
   5 lazy
   5 field_simplify
   5 fib
   5 beq_aux
   5 auto]
   4 true
   4 scard
   4 rename
   4 prove_lt_IZR
   4 iso
   4 is_suffix
   4 intersectl
   4 init_n
   4 idtac
   4 has_lt_irrefl
   4 eval
   4 eqq
   3 ys
   3 trivial]
   3 term
   3 ring]
   3 reg
   3 pn
   3 ok
   3 lt_first
   3 it
   3 intros[m]
   3 first_false
   3 field
   3 ex_take
   3 eo
   3 empty
   3 eauto
   3 double
   3 decoder
   3 decide
   3 bounded
   3 aBound
   2 xH
   2 tri
   2 trfib
   2 trailing_zeros
   2 total
   2 tcard
   2 sub_lists
   2 string
   2 setoid_replace
   2 prop_prime_dec
   2 proj
   2 prime_dec
   2 polyMult
   2 polyCalc
   2 pair_lt
   2 odd_S
   2 not_even_and_odd
   2 n^a
   2 le_S_n
   2 is_prime
   2 intros[L
   2 instantiate
   2 fun
   2 fourier
   2 fix
   2 find
   2 false
   2 even_odd_dec
   2 even_S
   2 eval_ops
   2 eauto]
   2 ds]
   2 ds
   2 discrR
   2 decn
   2 complement
   2 coll_gen
   2 cofix
   2 by
   2 beq
   2 autof
   2 autocol
   2 ack
   2 a_ring
   2 a^e
   1 yy
   1 y^
   1 x^n
   1 xO
   1 xI
   1 wpp
   1 well_def
   1 vars
   1 tailsF
   1 sumbool_not
   1 sum_f_R
   1 snd
   1 skip
   1 simple
   1 simpl]
   1 rep
   1 ps_intro
   1 ph
   1 npair
   1 nat_decidable
   1 m\
   1 lt_n_O
   1 lt_le_trans
   1 lt_S_n
   1 length
   1 le_lt_trans
   1 le_Sn_O
   1 iterate
   1 is
   1 intros[o
   1 intros[m
   1 intro]
   1 injective_sub
   1 h_inv
   1 get_r
   1 get_l
   1 fst
   1 from
   1 field_simplify_eq
   1 fibnext
   1 fib_eq_aux
   1 fb
   1 factor
   1 exist
   1 even_function
   1 env
   1 emit_code
   1 eexists
   1 econstructor
   1 divergent
   1 cutrewrite
   1 cosum
   1 convergent
   1 com
   1 col
   1 card_eq
   1 b^
   1 auto]]
   1 as
   1 andb_false_elim
   1 andb
   1 all_suffixes
   1 all_false
   1 add