Module prop::or

Tactics for Logical OR.

Functions

• assoc
  (a ∨ b) ∨ c => a ∨ (b ∨ c)
• both
  a ∨ a => a.
• bound_neg
  (¬a ∧ b) ∨ a => (b ∨ a).
• bound_pos
  (a ∧ b) ∨ ¬a => (b ∨ ¬a).
• distrib
  (a ∧ b) ∨ (a ∧ c) => a ∧ (b ∨ c)
• eq_nn
  ¬¬a == (a ∨ ¬¬a).
• from_de_morgan
  ¬(a ∧ b) => (¬a ∨ ¬b).
• in_left_arg
  (a ∨ b) ∧ (a => c) => (c ∨ b).
• in_right_arg
  (a ∨ b) ∧ (b => c) => (a ∨ c).
• symmetry
  a ∨ b => b ∨ a.
• to_de_morgan
  (¬a ∨ ¬b) => ¬(a ∧ b).