-- This is a comment
section forall_or_elim
    theorem forall_or_elim : ∀ (α : Type) (p q : α → Prop), ( ∀ x : α, p x ∧ q x ) → ∀ y : α, p y := 
    assume α : Type,
    assume p q : α → Prop, 
        assume h : ( ∀ x : α, p x ∧ q x ),
            assume y : α,
            show p y, from (h y).left
end forall_or_elim

section transitivity
    universe u
    variables (α : Type u) (r : α → α → Prop)
    variable  trans_r : ∀ {x y z}, r x y → r y z → r x z

    variables (a b c : α)
    variables (hab : r a b) (hbc : r b c)

    #check trans_r
    #check trans_r hab
    #check trans_r hab hbc
end transitivity

section and_comm
    lemma and_comm_one_way : Π a b : Prop, a ∧ b → b ∧ a := 
    λ (a b : Prop) (hab : a ∧ b) , and.intro (and.right hab) (and.left hab)

    theorem and_comm_full_1 : Π a b : Prop , a ∧ b ↔ b ∧ a := 
    λ (a b : Prop), iff.intro (and_comm_one_way a b) (and_comm_one_way b a) 

    theorem and_comm_full_2 : Π a b : Prop , a ∧ b ↔ b ∧ a := 
        assume a b : Prop, 
            let 
                forward := and_comm_one_way a b, 
                back := and_comm_one_way b a 
            in
            iff.intro forward back
end and_comm

-- The following is taken from https://leanprover.github.io/introduction_to_lean/
section sort
    universe u
    parameters {α : Type u} (r : α → α → Prop) [decidable_rel r]
    local infix `≼` : 50 := r

    def ordered_insert (a : α) : list α → list α
    | []       := [a]
    | (b :: l) := if a ≼ b then a :: (b :: l) else b :: ordered_insert l

    def insertion_sort : list α → list α
    | []       := []
    | (b :: l) := ordered_insert b (insertion_sort l)
end sort

#eval insertion_sort (λ m n : ℕ, m ≤ n) [5, 27, 221, 95, 17, 43, 7, 2, 98, 567, 23, 12]