natural-number-game

diff --git a/advanced-preposition.lean /dev/null
@@ -1,136 +0,0 @@
-example (P Q : Prop) (p : P) (q : Q) : P ∧ Q :=
-begin
-  split,
-  exact p,
-  exact q,
-end
-
-lemma and_symm (P Q : Prop) : P ∧ Q → Q ∧ P :=
-begin
-  intro h,
-  cases h with p q,
-  split,
-  exact q,
-  exact p,
-end
-
-lemma and_trans (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R :=
-begin
-  intro h1,
-  cases h1 with p _,
-  intro h2,
-  cases h2 with _ r,
-  split,
-  exact p,
-  exact r,
-end
-
-lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
-begin
-  intro p_iff_q,
-  cases p_iff_q with hpq hqp,
-  intro q_iff_r,
-  cases q_iff_r with hqr hrq,
-  split,
-  intro p,
-  apply hqr,
-  apply hpq,
-  exact p,
-  intro r,
-  apply hqp,
-  apply hrq,
-  exact r,
-end
-
-lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
-begin
-  intro p_iff_q,
-  cases p_iff_q with hpq hqp,
-  intro q_iff_r,
-  cases q_iff_r with hqr hrq,
-  split,
-  intro p,
-  apply hqr,
-  apply hpq,
-  exact p,
-  intro r,
-  apply hqp,
-  apply hrq,
-  exact r,
-end
-
-example (P Q : Prop) : Q → (P ∨ Q) :=
-  begin
-  intro q,
-  right,
-  exact q,
-end
-
-lemma or_symm (P Q : Prop) : P ∨ Q → Q ∨ P :=
-begin
-  intro h,
-  cases h with p q,
-  right,
-  exact p,
-  left,
-  exact q,
-end
-
-lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
-begin
-  split,
-  intro h,
-  have p := h.1,
-  cases h.2 with q r,
-  left,
-  split,
-  exact p,
-  exact q,
-  right,
-  split,
-  exact p,
-  exact r,
-  intro h,
-  cases h with p_and_q p_and_r,
-  cases p_and_q with p q,
-  split,
-  exact p,
-  left,
-  exact q,
-  cases p_and_r with p r,
-  split,
-  exact p,
-  right,
-  exact r,
-end
-
-lemma contra (P Q : Prop) : (P ∧ ¬ P) → Q :=
-begin
-  intro h,
-  rw not_iff_imp_false at h,
-  exfalso,
-  apply h.2,
-  exact h.1,
-end
-
-lemma contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
-begin
-  by_cases p : P; by_cases q : Q,
-  intros _ _,
-  exact q,
-  intro h,
-  have not_p := h q,
-  exfalso,
-  rw not_iff_imp_false at not_p,
-  apply not_p,
-  exact p,
-  intros _ _,
-  exact q,
-  intros h p,
-  have not_p := h q,
-  rw not_iff_imp_false at not_p,
-  exfalso,
-  apply not_p,
-  exact p,
-end
-

diff --git /dev/null b/advanced-proposition.lean
@@ -0,0 +1,136 @@
+example (P Q : Prop) (p : P) (q : Q) : P ∧ Q :=
+begin
+  split,
+  exact p,
+  exact q,
+end
+
+lemma and_symm (P Q : Prop) : P ∧ Q → Q ∧ P :=
+begin
+  intro h,
+  cases h with p q,
+  split,
+  exact q,
+  exact p,
+end
+
+lemma and_trans (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R :=
+begin
+  intro h1,
+  cases h1 with p _,
+  intro h2,
+  cases h2 with _ r,
+  split,
+  exact p,
+  exact r,
+end
+
+lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
+begin
+  intro p_iff_q,
+  cases p_iff_q with hpq hqp,
+  intro q_iff_r,
+  cases q_iff_r with hqr hrq,
+  split,
+  intro p,
+  apply hqr,
+  apply hpq,
+  exact p,
+  intro r,
+  apply hqp,
+  apply hrq,
+  exact r,
+end
+
+lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
+begin
+  intro p_iff_q,
+  cases p_iff_q with hpq hqp,
+  intro q_iff_r,
+  cases q_iff_r with hqr hrq,
+  split,
+  intro p,
+  apply hqr,
+  apply hpq,
+  exact p,
+  intro r,
+  apply hqp,
+  apply hrq,
+  exact r,
+end
+
+example (P Q : Prop) : Q → (P ∨ Q) :=
+  begin
+  intro q,
+  right,
+  exact q,
+end
+
+lemma or_symm (P Q : Prop) : P ∨ Q → Q ∨ P :=
+begin
+  intro h,
+  cases h with p q,
+  right,
+  exact p,
+  left,
+  exact q,
+end
+
+lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
+begin
+  split,
+  intro h,
+  have p := h.1,
+  cases h.2 with q r,
+  left,
+  split,
+  exact p,
+  exact q,
+  right,
+  split,
+  exact p,
+  exact r,
+  intro h,
+  cases h with p_and_q p_and_r,
+  cases p_and_q with p q,
+  split,
+  exact p,
+  left,
+  exact q,
+  cases p_and_r with p r,
+  split,
+  exact p,
+  right,
+  exact r,
+end
+
+lemma contra (P Q : Prop) : (P ∧ ¬ P) → Q :=
+begin
+  intro h,
+  rw not_iff_imp_false at h,
+  exfalso,
+  apply h.2,
+  exact h.1,
+end
+
+lemma contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
+begin
+  by_cases p : P; by_cases q : Q,
+  intros _ _,
+  exact q,
+  intro h,
+  have not_p := h q,
+  exfalso,
+  rw not_iff_imp_false at not_p,
+  apply not_p,
+  exact p,
+  intros _ _,
+  exact q,
+  intros h p,
+  have not_p := h q,
+  rw not_iff_imp_false at not_p,
+  exfalso,
+  apply not_p,
+  exact p,
+end
+

diff --git a/preposition.lean /dev/null
@@ -1,68 +0,0 @@
-example (P Q : Prop) (p : P) (h : P → Q) : Q :=
-begin
-  apply h,
-  exact p,
-end
-
-lemma imp_self (P : Prop) : P → P :=
-begin
-  intro p,
-  exact p,
-end
-
-lemma maze (P Q R S T U: Prop)
-           (p : P)
-           (h : P → Q)
-           (i : Q → R)
-           (j : Q → T)
-           (k : S → T)
-           (l : T → U) : U :=
-begin
-  apply l,
-  apply j,
-  apply h,
-  exact p,
-end
-
-example (P Q : Prop) : P → (Q → P) :=
-begin
-  intros p q,
-  exact p,
-end
-
-example (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
-begin
-  intros h1 h2 p,
-  apply h1,
-  exact p,
-  apply h2,
-  exact p,
-end
-
-lemma imp_trans (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) :=
-begin
-  intros hpq hqr p,
-  apply hqr,
-  apply hpq,
-  exact p,
-end
-
-lemma contrapositive (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
-begin
-  repeat {rw not_iff_imp_false},
-  intros hpq not_q p,
-  apply not_q,
-  apply hpq,
-  exact p,
-end
-
-example (A B C D E F G H I J K L : Prop)
-        ( f1 : A → B) ( f2 : B → E) ( f3 : E → D) 
-        ( f4 : D → A) ( f5 : E → F) ( f6 : F → C) 
-        ( f7 : B → C) ( f8 : F → G) ( f9 : G → J)
-        (f10 : I → J) (f11 : J → I) (f12 : I → H) 
-        (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L :=
-begin
-  cc,
-end
-

diff --git /dev/null b/proposition.lean
@@ -0,0 +1,68 @@
+example (P Q : Prop) (p : P) (h : P → Q) : Q :=
+begin
+  apply h,
+  exact p,
+end
+
+lemma imp_self (P : Prop) : P → P :=
+begin
+  intro p,
+  exact p,
+end
+
+lemma maze (P Q R S T U: Prop)
+           (p : P)
+           (h : P → Q)
+           (i : Q → R)
+           (j : Q → T)
+           (k : S → T)
+           (l : T → U) : U :=
+begin
+  apply l,
+  apply j,
+  apply h,
+  exact p,
+end
+
+example (P Q : Prop) : P → (Q → P) :=
+begin
+  intros p q,
+  exact p,
+end
+
+example (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
+begin
+  intros h1 h2 p,
+  apply h1,
+  exact p,
+  apply h2,
+  exact p,
+end
+
+lemma imp_trans (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) :=
+begin
+  intros hpq hqr p,
+  apply hqr,
+  apply hpq,
+  exact p,
+end
+
+lemma contrapositive (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
+begin
+  repeat {rw not_iff_imp_false},
+  intros hpq not_q p,
+  apply not_q,
+  apply hpq,
+  exact p,
+end
+
+example (A B C D E F G H I J K L : Prop)
+        ( f1 : A → B) ( f2 : B → E) ( f3 : E → D) 
+        ( f4 : D → A) ( f5 : E → F) ( f6 : F → C) 
+        ( f7 : B → C) ( f8 : F → G) ( f9 : G → J)
+        (f10 : I → J) (f11 : J → I) (f12 : I → H) 
+        (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L :=
+begin
+  cc,
+end
+