This gist shows how to create a GIF screencast using only free OS X tools: QuickTime, ffmpeg, and gifsicle.
To capture the video (filesize: 19MB), using the free "QuickTime Player" application:
Require Import Coq.NArith.NArith. | |
Theorem add_1_r : forall p, (p + 1)%positive = Pos.succ p. | |
Proof. | |
induction p; simpl; eauto. | |
Qed. | |
Theorem add_carry_spec : forall p q, Pos.add_carry p q = Pos.succ (p + q). | |
Proof. | |
induction p; induction q; simpl; eauto. |