Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment