BackgroundI am learning assistance, Coq, on my own. So far, I have completed reading Yves Bertot's Coq in a Hurry. Now, my goal is to prove some basic results concerning the natural numbers, culminating with the so-called division algorithm. However, I have encountered some setbacks on my way towards that goal. In particular, the two following results have proved (pun intended) to be more difficult to prove in Coq than I initially imagined. In fact, I have, after many fruitless attempts, resorted to prove them by hand (as shown below). This is clearly not helping me become more proficient in handling Coq; which is why I turn to this forum. My hope is that someone on this site is able and willing to help me translate my proofs below into a proof that Coq accepts. All help is sincerely appreciated!Theorem AFor all $x,y \in N$ \begin{equation} x < S(y) \subset x < y \lor \text{I}(N,x,y) \end{equation}Proof:Suppose $x < S(y)$. Hence there is a $z \in N$ with \begin{equation} \text{I}(N,x+S(z),S(y)) \tag{*}\end{equation}Hence by (Peano 1b and 3) \begin{equation} \text{I}(N,x+z,y) \end{equation}Define a predicate \begin{equation} Q(u):=(\text{I}(N,x+u,y) \subset x<y \lor \text{I}(N,x,y) \end{equation}It is sufficient to show $Q(z)$. We prove this by induction on $z$. To see $Q(0)$, not ethat if $\text{I}(N,x+0,y)$ holds then $\text{I}(N,x,y)$ is true by Peano 1a. Thus, $x<y \lor \text{I}(n,x,y)$. Now, we prove $Q(S(v))$: Suppose $\text{I}(N,x+S(v),y)$. From this definition we have $x<y$ and thus $x<y \lor \text{I}(N,x,y)$ also in this case. Finally, Peano's fifth axiom gives $Q(z)$ and by $(*)$ we get $x < y \lor \text{I}(N,x,y)$. \begin{equation} \tag{$\square$} \end{equation}Theorem BFor all $x,y \in N$ \begin{equation} x <y \lor \text{I}(N,x,y) \lor y<x \end{equation}Proof:If $x<y$ then $\neg \text{I}(N,x,y)$ by definition, and if $x>y$ then $\neg \text{I}(N,x,y)$ also by definition. If $x>y$ and $y>x$ then by transitivity and reflexivity, we have $\text{I}(N,x,y)$, which is a contradiction. Consequently, no more than one of the statements is true. We keep $y$ fixed and induct on $x$. When $\text{I}(N,0,y)$ we have $0 < y \lor \text{I}(N,0,y)$ for all $y$, which proves the base case. Next, suppose the theorem holds for $x$; now we want to prove the theorem for $S(x)$. From the trichotomy for $x$, there are three cases: $x<y,\text{I}(N,x,y)$, and $x>y$. If $x>y$, then clearly $S(x) >y$. If $\text{I}(N,x,y)$, then $S(x) >y$ (as $S(x) >x$ for all $x\in \mathbb{N}$). Finally, suppose $x <y$ Then, by theorem A we have $S(x) < y$ or $\text{I}(N,S(x),y)$, and in either case we are done.\begin{equation} \tag{$\square$} \end{equation}The theorems that I wish to prove, can be expressed as follows in Coq. Lemma less_lem (x y:N) :   less x (succ y) -> or (less x y) (I N x y).Theorem Ntrichotomy: (forall x y:N,   or (less x y) (or (I N x y) (less y x))).Useful resultsHere, I have gathered some of the results that I have defined, and proved up to this point. These are the ones that I refer to above. *This is the code that I have managed to write so far, note that most consists of definitions. *(* Sigma types *)Inductive Sigma (A:Set)(B:A -> Set) :Set :=  Spair: forall a:A, forall b : B a,Sigma A B.Definition E (A:Set)(B:A -> Set)  (C: Sigma A B -> Set)  (c: Sigma A B)  (d: (forall x:A, forall y:B x,       C (Spair A B x y))): C c :=match c as c0 return (C c0) with| Spair a b => d a bend. (* Binary sum type *)Inductive sum' (A B:Set):Set := inl': A -> sum' A B | inr': B -> sum' A B.Print sum'_rect.Definition D (A B : Set)(C: sum' A B -> Set)(c: sum' A B)(d: (forall x:A, C (inl' A B x)))(e: (forall y:B, C (inr' A B y))): C c :=match c as c0 return C c0 with| inl' x => d x| inr' y => e yend.(* Three useful finite sets *)Inductive N_0: Set :=.Definition R_0  (C:N_0 -> Set)  (c: N_0): C c :=match c as c0 return (C c0) withend.Inductive N_1: Set := zero_1:N_1.Definition R_1   (C:N_1 -> Set)  (c: N_1)  (d_zero: C zero_1): C c :=match c as c0 return (C c0) with  | zero_1 => d_zeroend.Inductive N_2: Set := zero_2:N_2 | one_2:N_2.Definition R_2   (C:N_2 -> Set)  (c: N_2)  (d_zero: C zero_2)  (d_one: C one_2): C c :=match c as c0 return (C c0) with  | zero_2 => d_zero  | one_2  => d_oneend.(* Natural numbers *)Inductive N:Set :=zero: N | succ : N -> N.Print N. Print N_rect.Definition R   (C:N -> Set)  (d: C zero)  (e: (forall x:N, C x -> C (succ x))):  (forall n:N, C n) :=fix F (n: N): C n :=  match n as n0 return (C n0) with  | zero => d  | succ n0 => e n0 (F n0)  end.(* Boolean to truth-value converter *)Definition Tr (c:N_2) : Set :=match c as c0 with  | zero_2 => N_0  | one_2 => N_1end.(* Identity type *)Inductive I (A: Set)(x: A) : A -> Set :=r :  I A x x.Print I_rect.Theorem J   (A:Set)  (C: (forall x y:A,               forall z: I A x y, Set))  (d: (forall x:A, C x x (r A x)))  (a:A)(b:A)(c:I A a b): C a b c.induction c.apply d.Defined.(* functions are extensional wrt  identity types *)Theorem I_I_extensionality (A B: Set)(f: A -> B):(forall x y:A, I A x y -> I B (f x) (f y)).Proof.intros x y P.induction P.apply r.Defined.(* addition *)Definition add (m n:N) : N  := R (fun z=> N) m (fun x y => succ y) n.(* multiplication *)Definition mul (m n:N) : N  := R (fun z=> N) zero (fun x y => add y m) n.(* Axioms of Peano verified *)Theorem P1a: (forall x: N, I N (add x zero) x).intro x.(* force use of definitional equality  by applying reflexivity *)apply r.Defined.Theorem P1b: (forall x y: N, I N (add x (succ y)) (succ (add x y))).intros.apply r.Defined.Theorem P2a: (forall x: N, I N (mul x zero) zero).intros.apply r.Defined.Theorem P2b: (forall x y: N, I N (mul x (succ y)) (add (mul x y) x)).intros.apply r.Defined.Definition pd (n: N): N :=R (fun _=> N) zero (fun x y=> x) n.(* alternativelyDefinition pd (x: N): N :=match x as x0 with  | zero => zero  | succ n0 => n0end.*)Theorem P3: (forall x y:N, I N (succ x) (succ y) -> I N x y).intros x y p.apply (I_I_extensionality N N pd (succ x) (succ y)).apply p.Defined.Definition not (A:Set): Set:= (A -> N_0).Definition isnonzero (n: N): N_2:=R (fun _ => N_2) zero_2 (fun x y => one_2) n.Theorem P4 : (forall x:N, not (I N (succ x) zero)).intro x.intro p.apply (J N (fun x y z =>     Tr (isnonzero x) -> Tr (isnonzero y))    (fun x => (fun t => t)) (succ x) zero).apply p.simpl.apply zero_1.Defined.Theorem P5 (P:N -> Set):P zero -> (forall x:N, P x -> P (succ x))   -> (forall x:N, P x).intros base step n.apply R.apply base.apply step.Defined.(* I(A,-,-) is an equivalence relation *)Lemma Ireflexive (A:Set): (forall x:A, I A x x).intro x.apply r.Defined.Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x).intros x y P.induction P.apply r.Defined.Lemma Itransitive (A:Set): (forall x y z:A, I A x y -> I A y z -> I A x z).intros x y z P Q.induction P.assumption.Defined.Lemma succ_cong : (forall m n:N, I N m n -> I N (succ m) (succ n)).intros m n H.induction H.apply r.Defined.Lemma zeroadd: (forall n:N, I N (add zero n) n).intro n.induction n.simpl.apply r.apply succ_cong.auto.Defined.Lemma succadd: (forall m n:N, I N (add (succ m) n) (succ (add m n))).intros.induction n.simpl.apply r.simpl.apply succ_cong.auto.Defined.Lemma commutative_add: (forall m n:N, I N (add m n) (add n m)).intros n m; elim n.apply zeroadd.intros y H; elim (succadd m y).simpl.rewrite succadd.apply succ_cong.assumption.Defined.Lemma associative_add: (forall m n k:N, I N (add (add m n) k) (add m (add n k))).intros m n k.induction k.simpl.apply Ireflexive.simpl.apply succ_cong.assumption.Defined.Definition or (A B : Set):= sum' A B.Definition less (m n: N) := Sigma N (fun z => I N (add m (succ z)) n).Lemma less_lem (x y:N) : less x (succ y) -> or (less x y) (I N x y).intro.destruct H.right.(* Here is where I'm working right now *)Defined.Theorem Ntrichotomy: (forall x y:N, or (less x y) (or (I N x y) (less y x))).
Theorem Proofs in Coq
automated theorem proving;proof assistants;mathematical programming;coq
Coq is a bit more cruel than paper proofs: when you write and we are done or clearly in a paper proof, there is often much more to do to convince Coq.Now I did a little clean up of your code, while trying to keep it in the same spirit. You can find it here.Several remarks:I used built in datatypes and definitions where I thought it wouldn't hurt your intent. Note that if I had used built-in equality instead of identity and the built in less-than relation, proofs would have been much easier, as many of your lemmas are in the database of known theorems, which are checked at each call ofauto with arith.I used some tactics you're probably not aware of, but a real Coq super-user would have much more powerful tactics at hand and written her own tactics to simplify the job. I always recommend CPDT as the place to learn about using tactics in a powerful manner.I used notations and tabbing to improve readability and built-in constructs like matching and the induction tactic to make things easier to prove and re-factor. In particular, your definition of less was hard to work with, you can see how I slightly modified it from$$ \exists x,\ m + (x+1) = n $$to the equivalent (but easier to use)$$ \exists x,\ (x + m)+1 = n$$this kind of definition tweaking happens a lot in formal proofs.While you may get answers to these kinds of questions here, I highly recommend you submit your work to Coq-Club which was created with the express purpose of answering these kinds of questions.