| Expression | Meaning | Prove it | Use it |
|---|---|---|---|
P -> Q |
implication | intro |
apply |
P /\ Q |
conjunction | split |
destruct |
P \/ Q |
disjunction | left, right |
destruct |
~ P |
negation | intro |
apply |
x = y |
equality | reflexivity, f_equal |
rewrite |
0 + 2 |
addition | simpl |
- |
n : nat |
natural numbers | constructor, exact 12 |
induction |
forall (x : A), B |
universal quantifier | intro |
apply, specialize |
exists (x : A), B |
existential quantifier | exists |
destruct |