コード例: 直観主義論理において，de morgan と弱い排中律が同値であること

[Seasawher]

def de_morgan := ∀ (p q : Prop), ¬(p ∧ q) → (¬p) ∨ (¬q)
  
def weak_em := ∀ (p : Prop), ¬ p ∨ ¬ ¬ p

theorem currying (p q : Prop) : ¬ (p ∧ q) ↔ (p → ¬ q) := by 
  constructor
  
  case mp =>
    intro h hp hq
    have : p ∧ q := ⟨hp, hq⟩
    contradiction

  case mpr =>
    intro h hand
    obtain ⟨hp, hq⟩ := hand
    have := h hp
    contradiction


theorem de_morgan_iff_weak_em : de_morgan ↔ weak_em := by
  constructor

  case mp =>
    intro h p
    have := h p
    apply this
    intro nand
    obtain ⟨hp, hnp⟩ := nand
    apply hnp
    assumption

  case mpr =>
    intro h p q hpq
    have em_p := h p
    have em_q := h q
    cases em_p
    case inl =>
      left; assumption
    case inr nnp =>
      cases em_q
      case inl => right; assumption
      case inr nnq =>
        exfalso
        apply nnp
        intro hp
        rw [currying] at hpq
        have := hpq hp
        contradiction

#print axioms de_morgan_iff_weak_em