Question 1:

When addition between natural numbers is defined as follows

Fixpoint add (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (add p m)
  end.

and the goal has the following shape 

  x, y, z : nat
  =========================
    add x (add y z) = add (add x y) z
What is the most efficient way to perform the proof by induction? the correct answer is answer no. 3: induction x as [ | x' IH].

Question 2:

With the following function 

Fixpoint f (n m : nat) : nat :=
  match n with
  | O => m
  | S p => f p (S m)
  end.
and the following goal 
  x, y : nat
  ============================
    f (S x) y = S (f y)
How should one start the proof by induction? the correct answer is answer no. 1: assert (main : forall m n, f (S m) n = S (f m n)). intros m; induction m as [|m' IH].

Question 3:

With function add defined as follows: 

Fixpoint add (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (add p m)
  end.
and the following goal: 
  x, y : nat
  ==============
    add (S (S x)) y = S (S (add x y))
How does one perform the proof? the correct answer is answer no. 3: reflexivity

Question 4:

With the function g defined as follows 

Fixpoint g n :=
  match n with
  | S (S p) => S (g p)
  | _ => 0
  end.
and the goal 
  x : nat
  ==================
    g x <= x
How does one start the proof? the correct answer is answer no. 4: assert (main : g x <= x /\ g (S x) <= S x). induction x as [| x' IH].