Require Import Coq.Bool.Bool. Require Import Coq.Arith.Arith. Require Import Coq.Arith.EqNat. Require Import Coq.omega.Omega. Require Import Coq.Lists.List. Import ListNotations. Fixpoint In {A : Type} (x : A) (l : list A) : Prop := match l with | [] => False | x' :: l' => x' = x \/ In x l' end. Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop := match l with | [] => True | x :: l' => P x /\ All P l' end. Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool := match l with | [] => true | x :: l' => andb (test x) (forallb test l') end. Theorem forallb_true_iff : forall X test (l : list X), forallb test l = true <-> All (fun x => test x = true) l. Proof. (* FILL IN HERE *) Admitted. Inductive le : nat -> nat -> Prop := | le_n : forall n, le n n | le_S : forall n m, (le n m) -> (le n (S m)). Notation "m <= n" := (le m n). Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o. Proof. (* FILL IN HERE *) Admitted. Theorem O_le_n : forall n, 0 <= n. Proof. (* FILL IN HERE *) Admitted. Theorem n_le_m__Sn_le_Sm : forall n m, n <= m -> S n <= S m. Proof. (* FILL IN HERE *) Admitted. Theorem Sn_le_Sm__n_le_m : forall n m, S n <= S m -> n <= m. Proof. (* FILL IN HERE *) Admitted. Theorem le_plus_l : forall a b, a <= a + b. Proof. (* FILL IN HERE *) Admitted. Theorem plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m. Proof. unfold lt. (* FILL IN HERE *) Admitted.