Choosing how to perform a proof

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

answer 1:

assert (main: forall m n, add x (add m n) = add (add x m) n).
induction x as [ | x' IH].

answer 2:

assert (main: forall m n p,
  add m (add n p) = add (add m n) p /\
  add (S m) (add n p) = add (add (S m) n) p).
induction m as [ | m' IH].

answer 3: induction x as [ | x' IH].

answer 4: induction z as [| z' 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.

  x, y : nat
  ============================
    f (S x) y = S (f y)

answer 1: assert (main : forall m n, f (S m) n = S (f m n)). intros m; induction m as [|m' IH].

answer 2: There is no need for a proof by induction. auto will do.

answer 3: induction y as [| y' IH].

answer 4: induction x as [| x' 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.

  x, y : nat
  ==============
    add (S (S x)) y = S (S (add x y))

answer 1:

assert (main : forall m n, add (S (S m)) n = S (S (add m n)) /\
            add (S (S (S m))) n = S (S (add (S m) n))).
  intros m; induction m as [ | m' IH]; intros n; simpl; try rewrite IH; auto.
destruct (main x y) as [H1 H2].
exact H1.

answer 2:

assert (main : forall m n, add (S (S m)) n = S (S (add m n))).
  intros m; induction m as [ | m' IH]; intros n; simpl; try rewrite IH; auto.
apply main.

answer 3: reflexivity

answer 4:

induction x as [| x' IH]; simpl; try rewrite IH; auto.

Question 4:

With the function g defined as follows

Fixpoint g n :=
  match n with
  | S (S p) => S (g p)
  | _ => 0
  end.

  x : nat
  ==================
    g x <= x

answer 1: lia

answer 2: simpl; auto.

answer 3: induction x as [| x' IH].

answer 4: assert (main : g x <= x /\ g (S x) <= S x). induction x as [| x' IH].