diff --git a/Basics.v b/Basics.v
index d5d3867..3c2b819 100644
--- a/Basics.v
+++ b/Basics.v
@@ -345,18 +345,35 @@ Compute (invert bw_white).
     over [simpl] and go directly to [reflexivity]. We'll explain
     what's happening later in the chapter. *)
 
-Definition nandb (b1:bool) (b2:bool) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition nandb (b1:bool) (b2:bool) : bool :=
+  match b1 with
+    | true => negb b2
+    | false => true
+  end.
 
 Example test_nandb1:               (nandb true false) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_nandb2:               (nandb false false) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_nandb3:               (nandb false true) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_nandb4:               (nandb true true) = false.
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
 
 (** **** Exercise: 1 star, standard (andb3)
 
@@ -364,18 +381,36 @@ Example test_nandb4:               (nandb true true) = false.
     return [true] when all of its inputs are [true], and [false]
     otherwise. *)
 
-Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
+  match b1, b2, b3 with
+  | true, true, true => true
+  | _, _, _ => false
+  end.
+
 
 Example test_andb31:                 (andb3 true true true) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_andb32:                 (andb3 false true true) = false.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_andb33:                 (andb3 true false true) = false.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_andb34:                 (andb3 true true false) = false.
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
 
 (* ================================================================= *)
 (** ** Types *)
@@ -816,14 +851,23 @@ Fixpoint exp (base power : nat) : nat :=
     factorial was not found in the current environment," it means
     you've forgotten the [:=]. *)
 
-Fixpoint factorial (n:nat) : nat
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint factorial (n:nat) : nat :=
+  match n with
+  | O => S O
+  | S p => mult (S p) (factorial p)
+  end.
 
 Example test_factorial1:          (factorial 3) = 6.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_factorial2:          (factorial 5) = (mult 10 12).
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
 
 (** Again, we can make numerical expressions easier to read and write
     by introducing notations for addition, subtraction, and
@@ -917,18 +961,36 @@ Proof. simpl. reflexivity.  Qed.
     function.  It can be done with just one previously defined
     function, but you can use two if you want. *)
 
-Definition ltb (n m : nat) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition ltb (n m : nat) : bool :=
+  if m <=? n then false else true.
+  (* match n, m with *)
+  (* | S n', S m' => ltb n' m' *)
+  (* | _, O => false *)
+  (* | O, _ => true *)
+  (* end. *)
+
 
 Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.
 
 Example test_ltb1:             (ltb 2 2) = false.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_ltb2:             (ltb 2 4) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
+
 Example test_ltb3:             (ltb 4 2) = false.
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 
 (* ################################################################# *)
 (** * Proof by Simplification *)
@@ -1091,8 +1153,10 @@ Proof.
 Theorem plus_id_exercise : forall n m o : nat,
   n = m -> m = o -> n + m = m + o.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros n m o H1 H2.
+  rewrite -> H1, H2.
+  reflexivity.
+Qed.
 
 (** The [Admitted] command tells Rocq that we want to skip trying
     to prove this theorem and just accept it as a given.  This is
@@ -1142,9 +1206,11 @@ Proof.
 Theorem mult_n_1 : forall p : nat,
   p * 1 = p.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros n.
+  rewrite <- mult_n_Sm.
+  rewrite <- mult_n_O.
+  reflexivity.
+Qed.
 
 (* ################################################################# *)
 (** * Proof by Case Analysis *)
@@ -1348,8 +1414,16 @@ Qed.
 Theorem andb_true_elim2 : forall b c : bool,
   andb b c = true -> c = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros b c.
+  destruct b eqn:Eb.
+  - simpl.
+    intros H.
+    rewrite <- H.
+    reflexivity.
+  - simpl.
+    intros H.
+    discriminate H.
+Qed.
 
 (** Before closing the chapter, we should mention one final
     convenience.  As you may have noticed, many proofs perform case
@@ -1389,8 +1463,10 @@ Qed.
 Theorem zero_nbeq_plus_1 : forall n : nat,
   0 =? (n + 1) = false.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros [].
+  - reflexivity.
+  - reflexivity.
+Qed.
 
 (* ================================================================= *)
 (** ** More on Notation (Optional) *)
@@ -1474,9 +1550,14 @@ Fixpoint plus' (n : nat) (m : nat) : nat :=
     homework assignment, make sure you comment out your solution so
     that it doesn't cause Rocq to reject the whole file!) *)
 
-(* FILL IN HERE
-
-    [] *)
+(*
+Fixpoint rejectme (a b: nat) : nat :=
+  match a, b with
+  | O, _ => b
+  | _, O => a
+  | S a', S b' => if even a then rejectme a' b else rejectme a b'
+  end.
+*)
 
 (* ################################################################# *)
 (** * More Exercises *)
@@ -1494,9 +1575,10 @@ Theorem identity_fn_applied_twice :
   (forall (x : bool), f x = x) ->
   forall (b : bool), f (f b) = b.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros f H b.
+  rewrite -> H, H.
+  reflexivity.
+Qed.
 
 (** **** Exercise: 1 star, standard (negation_fn_applied_twice)
 
@@ -1504,7 +1586,16 @@ Proof.
     to the previous one but where the hypothesis says that the
     function [f] has the property that [f x = negb x]. *)
 
-(* FILL IN HERE *)
+Theorem negation_fn_applied_twice :
+  forall (f : bool -> bool),
+  (forall (x : bool), f x = negb x) ->
+  forall (b : bool), f (f b) = b.
+Proof.
+  intros f H b.
+  rewrite -> H, H.
+  rewrite -> negb_involutive.
+  reflexivity.
+Qed.
 
 (* Do not modify the following line: *)
 Definition manual_grade_for_negation_fn_applied_twice : option (nat*string) := None.
@@ -1519,12 +1610,48 @@ Definition manual_grade_for_negation_fn_applied_twice : option (nat*string) := N
     [destruct] and [rewrite], but destructing everything in sight is
     not the best way.) *)
 
+Theorem orb_true : forall (b : bool), true || b = true.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem andb_true : forall (b : bool), true && b = b.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem orb_false : forall (b : bool), false || b = b.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem andb_false : forall (b : bool), false && b = false.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
 Theorem andb_eq_orb :
   forall (b c : bool),
   (andb b c = orb b c) ->
   b = c.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros b c H.
+  destruct b.
+  - rewrite andb_true, orb_true in H.
+    rewrite <- H.
+    reflexivity.
+  - rewrite andb_false, orb_false in H.
+    rewrite <- H.
+    reflexivity.
+Qed.
 
 (** [] *)
 
@@ -1627,8 +1754,13 @@ Compute letter_comparison B F.
 Theorem letter_comparison_Eq :
   forall l, letter_comparison l l = Eq.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  destruct l.
+  reflexivity.
+  reflexivity.
+  reflexivity.
+  reflexivity.
+  reflexivity.
+Qed.
 
 (** We can follow the same strategy to define the comparison operation
     for two grade modifiers.  We consider them to be ordered as
@@ -1658,29 +1790,34 @@ Definition modifier_comparison (m1 m2 : modifier) : comparison :=
     of a suitable call to [letter_comparison] to end up with just [3]
     possibilities. *)
 
-Definition grade_comparison (g1 g2 : grade) : comparison
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition grade_comparison (g1 g2 : grade) : comparison :=
+  match g1, g2 with
+  | Grade l1 m1, Grade l2 m2 =>
+    match letter_comparison l1 l2 with
+    | Gt => Gt
+    | Lt => Lt
+    | Eq => modifier_comparison m1 m2
+    end
+  end.
 
 (** The following "unit tests" of your [grade_comparison] function
     should pass once you have defined it correctly. *)
 
 Example test_grade_comparison1 :
   (grade_comparison (Grade A Minus) (Grade B Plus)) = Gt.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_grade_comparison2 :
   (grade_comparison (Grade A Minus) (Grade A Plus)) = Lt.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_grade_comparison3 :
   (grade_comparison (Grade F Plus) (Grade F Plus)) = Eq.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_grade_comparison4 :
   (grade_comparison (Grade B Minus) (Grade C Plus)) = Gt.
-(* FILL IN HERE *) Admitted.
-
-(** [] *)
+Proof. reflexivity. Qed.
 
 (** Now that we have a definition of grades and how they compare to
     one another, let us implement a late-penalty fuction. *)
@@ -1736,9 +1873,14 @@ Theorem lower_letter_lowers:
     letter_comparison F l = Lt ->
     letter_comparison (lower_letter l) l = Lt.
 Proof.
-(* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros l H.
+  destruct l.
+  - simpl. reflexivity.
+  - simpl. reflexivity.
+  - simpl. reflexivity.
+  - simpl. reflexivity.
+  - rewrite <- H. simpl. reflexivity.
+Qed.
 
 (** **** Exercise: 2 stars, standard (lower_grade)
 
@@ -1757,61 +1899,47 @@ Proof.
     cases.
 
     Our solution is under 10 lines of code total. *)
-Definition lower_grade (g : grade) : grade
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition lower_grade (g : grade) : grade :=
+  match g with
+  | Grade F Minus => Grade F Minus
+  | Grade l Plus => Grade l Natural
+  | Grade l Natural => Grade l Minus
+  | Grade l Minus => Grade (lower_letter l) Plus
+  end.
 
 Example lower_grade_A_Plus :
   lower_grade (Grade A Plus) = (Grade A Natural).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_A_Natural :
   lower_grade (Grade A Natural) = (Grade A Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_A_Minus :
   lower_grade (Grade A Minus) = (Grade B Plus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_B_Plus :
   lower_grade (Grade B Plus) = (Grade B Natural).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_F_Natural :
   lower_grade (Grade F Natural) = (Grade F Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_twice :
   lower_grade (lower_grade (Grade B Minus)) = (Grade C Natural).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_thrice :
   lower_grade (lower_grade (lower_grade (Grade B Minus))) = (Grade C Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 (** Rocq makes no distinction between an [Example] and a [Theorem]. We
     state the following as a [Theorem] only as a hint that we will use
     it in proofs below. *)
 Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = (Grade F Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
-
-(* GRADE_THEOREM 0.25: lower_grade_A_Plus *)
-(* GRADE_THEOREM 0.25: lower_grade_A_Natural *)
-(* GRADE_THEOREM 0.25: lower_grade_A_Minus *)
-(* GRADE_THEOREM 0.25: lower_grade_B_Plus *)
-(* GRADE_THEOREM 0.25: lower_grade_F_Natural *)
-(* GRADE_THEOREM 0.25: lower_grade_twice *)
-(* GRADE_THEOREM 0.25: lower_grade_thrice *)
-(* GRADE_THEOREM 0.25: lower_grade_F_Minus
-
-    [] *)
+Proof. reflexivity. Qed.
 
 (** **** Exercise: 3 stars, standard (lower_grade_lowers)
 
@@ -1830,9 +1958,10 @@ Theorem lower_grade_lowers :
     grade_comparison (Grade F Minus) g = Lt ->
     grade_comparison (lower_grade g) g = Lt.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros [].
+  simpl.
+  destruct l, m; simpl; intros H; apply H.
+Qed.
 
 (** Now that we have implemented and tested a function that lowers a
     grade by one step, we can implement a specific late-days policy.
@@ -1886,9 +2015,10 @@ Theorem no_penalty_for_mostly_on_time :
     (late_days <? 9 = true) ->
     apply_late_policy late_days g = g.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros.
+  rewrite -> apply_late_policy_unfold, H.
+  reflexivity.
+Qed.
 
 (** The following theorem states that, if a student has between 9 and
     16 late days, their final grade is lowered by one step. *)
@@ -1900,9 +2030,11 @@ Theorem grade_lowered_once :
     (late_days <? 17 = true) ->
     (apply_late_policy late_days g) = (lower_grade g).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros.
+  rewrite -> apply_late_policy_unfold, H, H0.
+  reflexivity.
+Qed.
 
-(** [] *)
 End LateDays.
 
 (* ================================================================= *)
@@ -1945,11 +2077,19 @@ Inductive bin : Type :=
     for binary numbers, and a function [bin_to_nat] to convert
     binary numbers to unary numbers. *)
 
-Fixpoint incr (m:bin) : bin
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint incr (m:bin) : bin :=
+  match m with
+  | Z => B1 Z
+  | B0 b => B1 b
+  | B1 b => B0 (incr b)
+  end.
 
-Fixpoint bin_to_nat (m:bin) : nat
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint bin_to_nat (m:bin) : nat :=
+  match m with
+  | Z => O
+  | B0 m' => 2 * (bin_to_nat m')
+  | B1 m' => S (2 * (bin_to_nat m'))
+  end.
 
 (** The following "unit tests" of your increment and binary-to-unary
     functions should pass after you have defined those functions correctly.
@@ -1958,29 +2098,27 @@ Fixpoint bin_to_nat (m:bin) : nat
     next chapter. *)
 
 Example test_bin_incr1 : (incr (B1 Z)) = B0 (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr2 : (incr (B0 (B1 Z))) = B1 (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr3 : (incr (B1 (B1 Z))) = B0 (B0 (B1 Z)).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr4 : bin_to_nat (B0 (B1 Z)) = 2.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr5 :
         bin_to_nat (incr (B1 Z)) = 1 + bin_to_nat (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr6 :
         bin_to_nat (incr (incr (B1 Z))) = 2 + bin_to_nat (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr7 : bin_to_nat (B0 (B0 (B0 (B1 Z)))) = 8.
-(* FILL IN HERE *) Admitted.
-
-(** [] *)
+Proof. reflexivity. Qed.
 
 (* ################################################################# *)
 (** * Optional: Testing Your Solutions *)