diff --git a/apl/README.org b/apl/README.org
new file mode 100644
index 0000000..1a11776
--- /dev/null
+++ b/apl/README.org
@@ -0,0 +1,9 @@
+#+TITLE: APL
+
+Tried with gnu-apl.
+
+Haven't yet used dyalog.
+
+ - hello.apl
+ - hello2.apl
+ - trigonometry.apl
diff --git a/apl/hello.apl b/apl/hello.apl
new file mode 100644
index 0000000..72353a5
--- /dev/null
+++ b/apl/hello.apl
@@ -0,0 +1,66 @@
+⍝ Set index origin so that ⍳ starts from 0
+⎕IO ← 0
+
+⍝ Print first 9 natural numbers
+⍝ ⍳ 9
+⍝ 0 1 2 3 4 5 6 7 8
+
+⍝ Reshape 9 numbers into 3x3 matrix
+⍝ 3 3 ρ ⍳ 9
+⍝ 0 1 2
+⍝ 3 4 5
+⍝ 6 7 8
+
+⍝ Seem to have created a mask
+⍝ (3 3 ρ ⍳ 9) ∈ 1 2 3 4 7
+⍝ 0 1 1
+⍝ 1 1 0
+⍝ 0 1 0
+
+⍝ Assigning to a variable r, I guess
+r ← (3 3 ρ ⍳ 9) ∈ 1 2 3 4 7
+
+⍝ Pad r towards right and bottom to make it a 5x7 matrix
+⍝ 5 7 ↑ r
+⍝ 0 1 1 0 0 0 0
+⍝ 1 1 0 0 0 0 0
+⍝ 0 1 0 0 0 0 0
+⍝ 0 0 0 0 0 0 0
+⍝ 0 0 0 0 0 0 0
+
+⍝ 'rotate by a vertical axis with ⌽'
+⍝ Looks like shifted the whole matrix towards the right by 2 columns. No, that's not it..
+⍝ ¯2 ⌽ 5 7 ↑ r
+⍝ 0 0 0 1 1 0 0
+⍝ 0 0 1 1 0 0 0
+⍝ 0 0 0 1 0 0 0
+⍝ 0 0 0 0 0 0 0
+⍝ 0 0 0 0 0 0 0
+
+⍝⍝⍝ 2 ⌽ 5 7 ↑ r
+⍝⍝⍝ 0 0 0 1 1 0 0
+⍝⍝⍝ 0 0 1 1 0 0 0
+⍝⍝⍝ 0 0 0 1 0 0 0
+⍝⍝⍝ 0 0 0 0 0 0 0
+⍝⍝⍝ 0 0 0 0 0 0 0
+⍝⍝⍝ 1 0 0 0 0 0 1
+⍝⍝⍝ 0 0 0 0 0 1 1
+⍝⍝⍝ 0 0 0 0 0 0 1
+⍝⍝⍝ 0 0 0 0 0 0 0
+⍝⍝⍝ 0 0 0 0 0 0 0
+
+
+⍝ 'Rotate around horizontal axis'
+R ← ¯1 ⊖ ¯2 ⌽ 5 7 ↑ r
+
+⍝ R R R
+
+⎕ ← data ← (1 2 3 4) (2 5 8 6) (8 6 2 3) (8 7 6 1)
+
+⍝⍝ Load a library function
+⍝⍝ )copy dfns disp
+
+
+
+
+)OFF
diff --git a/apl/hello2.apl b/apl/hello2.apl
new file mode 100644
index 0000000..92f64d0
--- /dev/null
+++ b/apl/hello2.apl
@@ -0,0 +1,25 @@
+⍝ Used gnuapl
+
+
+⍝ 10 ⌈ 20
+⍝ 20
+
+
+⍝ 1 2 3 ⌈  4 5
+⍝ LENGTH ERROR
+⍝       1 2 3⌈4 5
+⍝       ^    ^
+
+1 20 3 ⌈ 4 5 10
+4 20 10
+
+
+
+
+
+
+
+
+
+)OFF
+
diff --git a/apl/trigonometry.apl b/apl/trigonometry.apl
new file mode 100644
index 0000000..fb98686
--- /dev/null
+++ b/apl/trigonometry.apl
@@ -0,0 +1,25 @@
+⍝ https://aplwiki.com/wiki/Circular
+
+⍝ <operation> ○ <argument> 
+⍝ sin 0.5
+1 ○ 0.5
+
+⍝ sin 1.0
+1 ○ 1.0
+
+⍝ sin 0.0
+1 ○ 0
+
+⍝ pi π
+⍝ https://aplwiki.com/wiki/Pi_Times
+⍝ 1 times pi
+○1
+
+⍝ 2 times pi
+○2
+
+
+⍝ sin 30deg
+⍝ 1 ○ (○1 × 
+
+)OFF
diff --git a/coq/README.org b/coq/README.org
index b4fbc8a..4ddeaad 100644
--- a/coq/README.org
+++ b/coq/README.org
@@ -3,6 +3,7 @@
  - [[./sumn.v][sumn.v]]: Sum of first n natural numbers, their squares and cubes.
  - [[./de-morgan.v][de-morgan.v]]: de-Morgan's laws
  - [[./eqns.v][eqns.v]]: A 'hello world' using the 'equations' plugin
+ - [[./odd-even-prop.v][odd-even-prop.v]]: Parity of ~nat~ values
  - [[./cpdt/][cpdt/]]: stuff from the book CPDT
  - [[./sf/][sf]]: stuff from /Software foundations/
 
diff --git a/coq/odd-even-prop.v b/coq/odd-even-prop.v
new file mode 100644
index 0000000..c71d584
--- /dev/null
+++ b/coq/odd-even-prop.v
@@ -0,0 +1,104 @@
+Require Import Arith.
+
+(* Theorem about addition (Plus) *)
+Theorem OddOddEvenP: forall n m:nat,
+  Nat.Odd n -> Nat.Odd m -> Nat.Even (n+m).
+Proof.
+  intros n m Hp Hq.
+  destruct Hp as [p Hp].
+  destruct Hq as [q Hq].
+  unfold Nat.Even.
+  exists (p+q+1).
+  rewrite Nat.mul_add_distr_l.
+  rewrite Nat.mul_add_distr_l.
+  rewrite Nat.mul_1_r.
+  rewrite Hp.
+  rewrite Hq.
+  ring.
+Qed.
+
+Theorem OddEvenOddP: forall n m:nat,
+  Nat.Odd n -> Nat.Even m -> Nat.Odd (n+m).
+Proof.
+  intros n m [p Hp] [q Hq].
+  unfold Nat.Odd.
+  exists (p+q).
+  rewrite Nat.mul_add_distr_l.
+  rewrite Hp.
+  rewrite Hq.
+  ring.
+Qed.
+
+Theorem EvenEvenEvenP: forall n m:nat,
+  Nat.Even n -> Nat.Even m -> Nat.Even (n+m).
+Proof.
+  intros n m [p Hp] [q Hq].
+  unfold Nat.Even.
+  exists (p+q).
+  rewrite Nat.mul_add_distr_l.
+  rewrite Hp.
+  rewrite Hq.
+  ring.
+Qed.
+
+
+(* Theorem about subtraction (Minus) *)
+Theorem OddOddEvenM: forall n m:nat,
+  Nat.Odd n -> Nat.Odd m -> Nat.Even (n-m).
+Proof.
+  intros n m [p Hp] [q Hq].
+  unfold Nat.Even.
+  exists (p-q).
+  rewrite Nat.mul_sub_distr_l.
+  rewrite Hp.
+  rewrite Hq.
+  (* doing [lia] here would solve this goal *)
+  simpl.
+  rewrite Nat.add_0_r.
+  rewrite Nat.add_0_r.
+  rewrite (Nat.add_comm (q+q) 1).
+  replace (p + p + 1) with (1 + p + p) by ring.
+  Print Nat.sub.
+  simpl.
+  reflexivity.
+Qed.
+
+Theorem EvenEvenEvenM: forall n m:nat,
+  Nat.Even n -> Nat.Even m -> Nat.Even (n-m).
+Proof.
+  intros n m [p Hp] [q Hq].
+  unfold Nat.Even.
+  exists (p-q).
+  rewrite Hp.
+  rewrite Hq.
+  rewrite Nat.mul_sub_distr_l.
+  reflexivity.
+Qed.
+
+Require Import Lia.
+(* 1-2 is 0 but is even. So m<=n constraint has to be there *)
+Theorem OddEvenOddM: forall n m:nat,
+  Nat.Odd n -> Nat.Even m -> m<=n -> Nat.Odd (n-m).
+Proof.
+  intros n m [p Hp] [q Hq] H.
+  unfold Nat.Odd.
+  exists (p-q).
+  rewrite Hp.
+  rewrite Hq.
+  rewrite Nat.mul_sub_distr_l.
+  replace (2*p+1) with (1+2*p) by ring.
+  rewrite (Nat.add_comm (2*p-2*q) 1).
+  SearchRewrite (_ + (_ - _)).
+  rewrite Nat.add_sub_assoc.
+  - reflexivity.
+  - lia.
+
+Restart.
+  (* Another way *)
+  (* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/lia.20shows.20error.2E *)
+  (* Thanks to Pierre Castéran *)
+  intros n m [p Hp] [q Hq] H.
+  subst.
+  exists (p-q).
+  lia.
+Qed.