diff --git a/pascal-prh.v b/pascal-prh.v
new file mode 100644
index 0000000..fb8fe50
--- /dev/null
+++ b/pascal-prh.v
@@ -0,0 +1,485 @@
+Require Import Ring.
+Require Import ArithRing.
+
+(* Coq is like Lisp in that it is so powerful, that every user tends to invent
+   a whole new programming language using its features. This makes Lisp by
+   itself an easy tool to misuse, but constrained by an application like CAD or
+   Emacs, it becomes quite a powerful approach for implementing a small
+   language.
+
+   The goal of this file is to consciously and deliberately create a new
+   dialect of proof assistant, constrained by the goal that the proofs should
+   explain themselves as they go, without requiring an IDE, the same way that
+   real life math proofs explain themselves as you read them.
+
+   The two main things that stop an 'idiomatic' Coq proof from being readable
+   without an IDE, are heavy reliance on proof automation, and hidden state
+   that varies from line to line in other terse and clever ways. In general the
+   philosophy of many Coq proofs is, the computer has checked it, so who cares
+   why it is true? This is not going to be our philosophy.
+
+   For an example of both of these weaknesses at their maximum, consider the
+   following Coq proof: *)
+
+Theorem not_not_law_of_excluded_middle: forall A: Prop,
+  not (not (A \/ not A)).
+Proof.
+  intros A H.
+  assert (not A); auto.
+Qed.
+
+(* How does this proof work? Who knows! You'll havelhs to run `debug auto`
+   yourself and see. Lots of effort has been put into this sort of automation,
+   in fact, the entire proof above could havelhs been replaced with a single
+   'intuition' tactic, which specializes in intuitionist logic tautologies.
+
+   While it is useful to know that Coq *can* go that far with automation, it is
+   important that we remain tasteful in how we apply it. Proofs are meant to
+   convince the reader, and ideally to inform them as well. "Look! It type
+   checks!" is convincing, but not informative.
+
+   We will find that proof automation comes in very handy when doing routine
+   algebraic manipulations, but apart from that, the more explicit we can make
+   our control flow, the more informative (and thus useful) our proofs will be.
+
+   As an example, let's look at a useful but surprisingly involved inductive
+   proof, that all numbers are either even or odd. First let's define what we
+   mean by even and odd. *)
+
+(* A number is even if it is equal to some other number, doubled. *)
+
+Definition Even (n: nat): Prop :=
+  exists k: nat, n = 2 * k.
+
+(* And a number is odd if it is one more than that. *)
+
+Definition Odd (n: nat): Prop :=
+  exists k: nat, n = 2 * k + 1.
+
+(* Let's try proving a number is even. We'll do zero, since then we havelhs a base
+   case for induction later. *)
+
+Lemma zero_is_even: Even 0.
+Proof.
+  (* We need to find a k so that 2 * k = 0. Let's try.... 0 *)
+  exists 0.
+  (* Now to show that 2 * 0 = 0, we let Coq beta/eta reduce it to 0 = 0, and
+     then fall back to 'reflexivity', the defining property of Leibniz equality. *)
+  reflexivity.
+Qed.
+
+(* It is annoying that we havelhs to write all of these comments to explain what
+   the state of the proof assistant is *going* to be. Plus, these comments can
+   get out of sync with the program, which seems absurd in a language
+   specifically designed to check such things. Let's make some new tactics to
+   let us represent this information better. *)
+
+(* This first tactic lets us start such a string of manipulations, by declaring
+   what the LHS of our goal is, effectively just a comment, but checked. *)
+Ltac havelhs expr :=
+  lazymatch goal with
+  | |- ?Rel expr ?R =>
+    idtac
+  | |- ?Rel ?L ?R =>
+    fail "Have annotation. Expected" expr "but got" L
+  | |- ?Other =>
+    fail "Goal is not a relation. Goal:" Other
+  end.
+
+(* Next, all manipulations are ultimately built out of beta/eta equivalence,
+   so let's make a tactic to check these equivalences for us. *) 
+Ltac basic_lambda_calculus_tells_us_the_lhs_is expr :=
+  lazymatch goal with
+  | |- ?Rel ?L ?R =>
+    unify L expr;
+    change_no_check (Rel expr R)
+  | |- ?Other =>
+    fail "Goal is not a relation. Goal:" Other
+  end.
+
+(* Using basic_lambda_calculus_tells_us_the_lhs_is makes it easy to annotate how an expression simplifies as it is
+   reduced, but sometimes we need to show how the RHS simplifies as well, so
+   let's make a tactic to break up an equation into two parts, showing how each
+   side equals some simpler intermediate value. *)
+Ltac both_sides_equal expr :=
+  transitivity expr; [ | symmetry].
+
+(* Finally, if we want to be sure that our above annotations are correct, this
+   tactic will check that the LHS and RHS are not just equivalent, but already
+   identical. *)
+Ltac obvious :=
+  lazymatch goal with
+  | |- ?Rel ?L ?L =>
+    reflexivity
+  | |- ?Rel ?L ?R =>
+    fail "Chain derivation not obvious. Left:" L "Right:" R
+  | |- ?Other =>
+    fail "Goal is not a relation. Goal:" Other
+  end.
+
+(* Let's try again at that simple zero example, but with annotations. *)
+
+Lemma zero_is_even_explicit: Even 0.
+Proof.
+  (* We still need to pick a value for k. *)
+  exists 0.
+  (* Now let's prove our goal a little more explicitly. *)
+  both_sides_equal 0.
+  -havelhs 0.
+   obvious.
+  -havelhs (2 * 0).
+   basic_lambda_calculus_tells_us_the_lhs_is 0.
+   obvious.
+Qed.
+
+(* This case might be sort of overkill... As one gains/regains familiarity with
+   DTT, statements like "eq_refl is a proof that 0 = 2 * 0" becomes totally
+   intuitive, but still, these tactics hopefully explain why.
+
+   Now let's do something where this is a little less overkill, showing that if
+   a number is even, then the next number is odd.
+
+   S is the successor, in Peano arithmetic, and inductive proofs. *)
+
+Lemma even_implies_odd: forall n: nat,
+  Even n -> Odd (S n).
+Proof.
+  intros n IsEven.
+  destruct IsEven as [k Eq].
+  (* n is 2 * k, so n+1 is 2 * k + 1, so k is the value we need to prove that
+     n+1 is odd. 'exists' is a tactic that says a term should be taken as the
+     term we are trying to prove exists. *)
+  exists k.
+  (* Now we actually havelhs to prove that S n = 2 * k + 1, though. *)
+  havelhs (S n).
+  rewrite Eq.
+  havelhs(S (2 * k)).
+  basic_lambda_calculus_tells_us_the_lhs_is (1 + 2 * k).
+  (* This is almost what we want. Let's do a commutativity rewrite. *)
+  rewrite (PeanoNat.Nat.add_comm _ _).
+  havelhs(2 * k + 1).
+  obvious.
+Qed.
+
+(* Having these tactics definitely makes the control flow easier to follow, but
+   it would be nice if we didn't havelhs to appeal to the laws of associativity
+   and commutativity every time our goal was expressed slightly differently to
+   what we expected. Let's take some of those powerful proof automation tools,
+   and use them for this very narrow task of algebraic manipulation. *)
+
+Ltac basic_algebra_tells_us_the_lhs_is expr :=
+  lazymatch goal with
+  | |- ?Rel ?L ?R =>
+    transitivity expr; [> ring | ]
+  | |- ?Other =>
+    fail "Goal is not a relation. Goal:" Other
+  end.
+
+(* Further, manipulating existence proofs using exists and destruct is a bit
+   hard to follow. Let's make some tactics for declaring what we know, and what
+   we havelhs to prove, as each of these things change from line to line. *)
+
+(* If our goal isn't a relation yet, we might still want to declare it. *)
+Ltac havegoal expr :=
+  lazymatch goal with
+  | |- expr =>
+    idtac
+  | |- ?Other =>
+    fail "Expected goal to be" expr "but it was" Other
+  end.
+
+(* The place where we learn new equations is often quite far from where we
+   use them. This tactic lets us state in-context what hypothesis we are
+   using, and defer choosing a name for it until then as well. *)
+Ltac weknow newid P :=
+  lazymatch goal with
+  | proof: P |- ?Goal =>
+    rename proof into newid
+  | |- ?Goal =>
+    fail "Knowledge assertion. Cannot find proof of" P
+  end.
+
+Tactic Notation "weknow" ident(newid) ":" constr(P) :=
+  weknow newid P.
+
+(* We're going to need these for odd_implies_even, as that case is harder! *)
+
+Lemma odd_implies_even: forall n: nat,
+  Odd n -> Even (S n).
+Proof.
+  intros.
+  weknow IsOdd: (Odd n).
+  destruct IsOdd as [k].
+  havegoal (Even (S n)).
+  weknow OddEq: (n = 2 * k + 1).
+  (* When we do goal manipulations like 'exists', let's annotate the new goal
+     on the same line using the semicolon separator. *)
+  unfold Even.
+  exists (S k).
+  havegoal (S n = 2 * S k).
+  both_sides_equal (2 * k + 2).
+  -havelhs (S n).
+   (* Let's also annotate rewrites on the same line, if it will fit. *)
+   rewrite OddEq; havelhs (S (2 * k + 1)).
+   (* We should get used to S as a first-class operation, since this is Peano
+      arithmetic, at the end of the day. But for now we will get rid of the S
+      and apply algebraic manipulations to more traditional expressions. *)
+   basic_lambda_calculus_tells_us_the_lhs_is (1 + 2 * k + 1).
+   (* Now let's get Coq to prove our algebra for us! *)
+   basic_algebra_tells_us_the_lhs_is (2 * k + 2).
+   obvious.
+  -havelhs (2 * S k).
+   (* Again, get rid of the S. *)
+   basic_lambda_calculus_tells_us_the_lhs_is (2 * (1 + k)).
+   (* And basic_algebra_tells_us_the_lhs_is. *)
+   basic_algebra_tells_us_the_lhs_is (2 * k + 2).
+   obvious.
+Qed.
+
+(* You might see where this is going now. We havelhs all the pieces to build an
+   inductive proof! *)
+
+Theorem even_or_odd: forall n: nat,
+  Even n \/ Odd n.
+Proof.
+  intro n.
+  induction n.
+  (* To prove something inductively, we havelhs to prove it is true for 0, and
+     then that it is true for any number of the form S n. *)
+  *havegoal (Even 0 \/ Odd 0).
+   left; havegoal (Even 0).
+   exact zero_is_even.
+  *havegoal (Even (S n) \/ Odd (S n)).
+   weknow Ind: (Even n \/ Odd n).
+   (* To prove that S n is even or odd, we need to know which case we are in
+      when it comes to n being even or odd. *)
+   destruct Ind.
+   +weknow IsEven: (Even n).
+    havegoal (Even (S n) \/ Odd (S n)).
+    (* We can use the 'left' and 'right' tactics to choose how we are going to
+       prove a dysjunction. *)
+    right; havegoal (Odd (S n)).
+    (* We are appealing to a lemma, so get the Curry-Howard proof object for
+       that lemma, and apply it to produce the 'exact' proof we need. *)
+    exact (even_implies_odd n IsEven).
+   +weknow IsOdd: (Odd n).
+    havegoal (Even (S n) \/ Odd (S n)).
+    (* Very similar logic on the other side. *)
+    left; havegoal (Even (S n)).
+    exact (odd_implies_even n IsOdd).
+Qed.
+
+(* Wasn't that a fun and pleasant adventure?
+
+   So we see that more explicit control flow sets us up for quite nice proofs,
+   where we can see that the goal follows by basic algebra, algebra which Coq
+   is prepared to do for us.
+
+   Agda and Idris programmers will recognize that Even and Odd could havelhs been
+   jerry-rigged so that the `ring` tactics weren't required at all, and while
+   we will be exploiting that sort of trick to simplify things when they get
+   hard, it's useful to embrace these un-optimized definitions when trying to
+   demonstrate Coq tactics. *)
+
+
+
+(* Now, finally, let's get on with some number theory! First let's look at
+   Pascal's triangle, since understanding that turns out to be essential to
+   understanding how to find points on elliptic curves.
+
+   Our way of indexing Pascal's triangle is going to be a little weird, though;
+   in order to avoid having to make special cases for all the zeros to the left
+   and right of the triangle, we will index the triangle in diagonal strips, so
+   e.g. 
+     pascal 0 _ = 1
+     pascal 1 k = k
+     pascal 2 k = k*(k+1)/2
+     pascal 3 k = k*(k+1)*(k+2)/6
+   etc.
+
+   To do this without getting horny over nested cases, let's get horny over
+   higher order functions instead. Let's define a function that takes a
+   sequence, and returns a sequence representing the partial sums of that
+   sequence. *)
+
+Fixpoint partial_sum (seq: nat -> nat) (count: nat): nat :=
+  match count with
+  | O => 0
+  | S count' => partial_sum seq count' + seq count'
+  end.
+
+(* But Triangular numbers aren't the sum of 0 or more numbers, they are the sum
+   of one or more numbers! So let's also define a 'series' variation. *)
+
+Definition series (seq: nat -> nat) (index: nat): nat :=
+  partial_sum seq (1 + index).
+
+Fixpoint pascal (r: nat): nat -> nat :=
+  match r with
+  | 0 => fun _ => 1
+  | S r' => series (pascal r')
+  end.
+
+(* Now the first 'row' of our function is all 1 by definition, but it is useful
+   to show that the first 'column' is all 1 as well. *)
+
+Lemma pascal_0: forall r: nat,
+  pascal r 0 = 1.
+Proof.
+  intro r.
+  induction r.
+  *havelhs (pascal 0 0).
+   basic_lambda_calculus_tells_us_the_lhs_is 1.
+   obvious.
+  *havelhs (pascal (S r) 0).
+   basic_lambda_calculus_tells_us_the_lhs_is (series (pascal r) 0).
+   basic_lambda_calculus_tells_us_the_lhs_is (pascal r 0).
+   (* Let's stop this chain reasoning here, and look at what our goal is now. *)
+   havegoal (pascal r 0 = 1).
+   weknow Ind: (pascal r 0 = 1).
+   exact Ind.
+Qed.
+
+(* Next let's define some combinatoric functions, and see if we can't prove how
+   they relate to the recursive formula above. *)
+
+Fixpoint factorial (n : nat): nat :=
+  match n with
+  | S n' => n * factorial n'
+  | O => 1
+  end.
+
+Fixpoint prod_up (k r: nat): nat :=
+  match k with
+  | 0 => 1
+  | S k' => prod_up k' (1 + r) * r
+  end.
+
+(* Often this permutation prod_up is notated as factorial (k + r) / factorial k,
+   but we don't havelhs division in peano arithmetic, so let's show this relation
+   through multiplication instead. *)
+
+Lemma prod_up_ratio: forall k r: nat,
+  prod_up k (1 + r) * factorial r = factorial (k + r).
+Proof.
+  intros k.
+  induction k; intro r.
+  *both_sides_equal (factorial r).
+   -basic_lambda_calculus_tells_us_the_lhs_is (1 * factorial r).
+    basic_algebra_tells_us_the_lhs_is (factorial r).
+    obvious.
+   -havelhs (factorial (0 + r)).
+    basic_lambda_calculus_tells_us_the_lhs_is (factorial r).
+    obvious.
+  *havelhs (prod_up (S k) (1 + r) * factorial r).
+   basic_lambda_calculus_tells_us_the_lhs_is (prod_up k (2 + r) * (1 + r) * factorial r).
+   weknow Ind: (forall r': nat, prod_up k (1 + r') * factorial r' = factorial (k + r')).
+   basic_algebra_tells_us_the_lhs_is (prod_up k (2 + r) * ((1 + r) * factorial r)).
+   basic_lambda_calculus_tells_us_the_lhs_is (prod_up k (1 + (1 + r)) * factorial (1 + r)).
+   pose (NigFace := Ind (1 + r)).
+   rewrite NigFace.
+   havelhs (factorial (k + (1 + r))).
+   basic_lambda_calculus_tells_us_the_lhs_is (factorial (k + S r)).
+   (* Use one of those manual manipulations, since the term we are manipulating
+      is inside of a function call, so ring will get confused. *)
+   rewrite <- (plus_n_Sm k r).
+   havelhs (factorial (S (k + r))).
+   basic_lambda_calculus_tells_us_the_lhs_is (factorial (S k + r)).
+   obvious.
+Qed.
+
+(* If we let r = 0 then we even show that the factorial is a special case of
+   this product function. *)
+Lemma factorial_up: forall n: nat,
+  prod_up n 1 = factorial n.
+Proof.
+  intro n.
+  havelhs (prod_up n 1).
+  basic_algebra_tells_us_the_lhs_is (prod_up n 1 * 1).
+  basic_lambda_calculus_tells_us_the_lhs_is (prod_up n (1 + 0) * factorial 0).
+  pose (Foo := prod_up_ratio n 0).
+  rewrite Foo; havelhs (factorial (n + 0)).
+  rewrite <- (plus_n_O); havelhs (factorial n).
+  obvious.
+Qed.
+
+(* Another trick that is implicit in pen-and-paper notation, that we havelhs to be
+   explicit about in code, is the fact that we can pull terms off of either
+   side of this product, to do algebraic manipulations with. *)
+
+Lemma prod_up_down: forall k r: nat,
+  prod_up (1 + k) r = (k + r) * prod_up k r.
+Proof.
+  intro k.
+  induction k; intro r.
+  *both_sides_equal r.
+   -basic_lambda_calculus_tells_us_the_lhs_is (prod_up 1 r).
+    basic_lambda_calculus_tells_us_the_lhs_is (r + 0).
+    basic_algebra_tells_us_the_lhs_is r.
+    obvious.
+   -basic_lambda_calculus_tells_us_the_lhs_is (r * prod_up 0 r).
+    basic_lambda_calculus_tells_us_the_lhs_is (r * 1).
+    basic_algebra_tells_us_the_lhs_is r.
+    obvious.
+  *havelhs (prod_up (1 + S k) r).
+   basic_lambda_calculus_tells_us_the_lhs_is (prod_up (1 + k) (1 + r) * r).
+   weknow Ind: (forall r': nat, prod_up (1 + k) r' = (k + r') * prod_up k r').
+   pose (Foo := Ind (1 + r)).
+   rewrite Foo.
+   havelhs ((k + (1 + r)) * prod_up k (1 + r) * r).
+   basic_algebra_tells_us_the_lhs_is ((S k + r) * (prod_up k (1 + r) * r)).
+   basic_lambda_calculus_tells_us_the_lhs_is ((S k + r) * prod_up (S k) r).
+   obvious.
+Qed.
+
+(* Now let's get to the theorem! I haven't broken this one up at all. Turn your
+   font up or something. *)
+
+Theorem pascal_choose: forall r k: nat,
+  pascal r k * factorial k = prod_up k (S r).
+Proof.
+  intro r.
+  induction r; intro k.
+  *basic_lambda_calculus_tells_us_the_lhs_is (1 * factorial k).
+   basic_algebra_tells_us_the_lhs_is (factorial k).
+   pose (Foo := factorial_up k).
+   symmetry.
+   exact Foo. 
+  *induction k.
+  **basic_lambda_calculus_tells_us_the_lhs_is (pascal (S r) 0 * 1).
+    basic_algebra_tells_us_the_lhs_is (pascal (S r) 0).
+    pose (Foo := pascal_0 (S r)).
+    both_sides_equal 1.
+    -exact Foo.
+    -basic_lambda_calculus_tells_us_the_lhs_is 1.
+     obvious.
+  **havelhs (pascal (S r) (S k) * factorial (S k)).
+    basic_lambda_calculus_tells_us_the_lhs_is ((pascal (S r) k + pascal r (S k)) * factorial (S k)).
+    weknow IndR: (forall k': nat, pascal r k' * factorial k' = prod_up k' (S r)).
+    (* We havelhs a pascal r (S k) and a factorial (S k), let's get them together. *)
+    basic_algebra_tells_us_the_lhs_is (pascal (S r) k * factorial (S k) + pascal r (S k) * factorial (S k)).
+    rewrite (IndR (S k)).
+    havelhs (pascal (S r) k * factorial (S k) + prod_up (S k) (S r)).
+    (* Good. Now, look for similar to apply to pascal (S r) k *)
+    weknow IndK: (pascal (S r) k * factorial k = prod_up k (S (S r))).
+    (* So we need factorial k. That can be arranged. *)
+    basic_lambda_calculus_tells_us_the_lhs_is (pascal (S r) k * (S k * factorial k) + prod_up (S k) (S r)).
+    basic_algebra_tells_us_the_lhs_is (S k * (pascal (S r) k * factorial k) + prod_up (S k) (S r)).
+    rewrite (IndK).
+    havelhs (S k * prod_up k (S (S r)) + prod_up (S k) (S r)).
+    (* This is good. All the factorial pascal stuff is gone. Now we just need
+       to factorise these big products. They are pretty close already. *)
+    basic_lambda_calculus_tells_us_the_lhs_is (S k * prod_up k (S (S r)) + prod_up k (S (S r)) * S r).
+    (* Let's rewrite these S's. *)
+    basic_lambda_calculus_tells_us_the_lhs_is ((1 + k) * prod_up k (2 + r) + prod_up k (2 + r) * (1 + r)).
+    (* And collect! *)
+    basic_algebra_tells_us_the_lhs_is ((k + (2 + r)) * prod_up k (2 + r)).
+    symmetry.
+    basic_lambda_calculus_tells_us_the_lhs_is (prod_up (S k) (2 + r)).
+    pose (Foo := prod_up_down k (2 + r)).
+    basic_lambda_calculus_tells_us_the_lhs_is (prod_up (1 + k) (2 + r)).
+    exact Foo.
+Qed.
+
+
+