Require Import NaturalDeduction. Require Import PeanoNat. Import Nat. Lemma L1 : forall n : nat, 2*(S n) <= 2^(S n). Proof. induction n. simpl. apply le_refl. rewrite mul_succ_r. rewrite pow_succ_r'. rewrite (mul_succ_l 1 (2^S n)). rewrite mul_1_l. apply add_le_mono. assumption. rewrite <- (pow_1_r 2) at 1. apply pow_le_mono_r. apply neq_succ_0. apply le_n_S. apply le_0_n. Qed. Require Import Factorial. Lemma L2 : forall n : nat, fact n <= n^n. Proof. induction n. simpl. apply le_refl. simpl. rewrite <- (mul_1_l (fact n)) at 1. rewrite <- mul_add_distr_r. rewrite <- (mul_1_l (S n^n)) at 1. rewrite <- mul_add_distr_r. apply mul_le_mono_l. rewrite IHn. apply pow_le_mono_l. apply le_succ_diag_r. Qed. Require Import List. Import ListNotations. Lemma L3 (A : Type) : forall l1 l2 : list A, length (l1 ++ l2) = length l1 + length l2. Proof. induction l1. Forall_Intro. simpl. trivial. Forall_Intro. simpl. rewrite IHl1. trivial. Qed. Lemma L4 (A : Type) : forall l : list A, rev (rev l) = l. Proof. induction l. simpl. trivial. simpl. rewrite rev_unit. rewrite IHl. trivial. Qed. Lemma L5 (A : Type) : forall l1 l2 : list A, rev (l1 ++ l2) = rev l2 ++ rev l1. Proof. induction l1. Forall_Intro. simpl. rewrite app_nil_r. trivial. Forall_Intro. simpl. rewrite IHl1. rewrite <- app_assoc. trivial. Qed. Lemma L6 (A : Type) : forall (l1 l2 : list A) (a : A), In a (l1 ++ l2) -> In a l1 \/ In a l2. Proof. induction l1. Forall_Intro. Forall_Intro. simpl. Impl_Intro. Or_Intro_2. assumption. Forall_Intro. Forall_Intro. simpl. Impl_Intro. Or_Elim in H. Or_Intro_1. Or_Intro_1. assumption. Forall_Elim in IHl1 with l2. Forall_Elim in H1 with a0. Impl_Elim in H2 and H. Or_Elim in H3. Or_Intro_1. Or_Intro_2. assumption. Or_Intro_2. assumption. Qed.