add that simplify from both sides in Coq

AddCommutativity.v

(* this is the commutativity on Nat.add (the builtin + in Coq) that only simplifies
   from the left *)
Theorem add_comm : forall (n m : nat), n + m = m + n.
  assert (plus_0_r : forall (n' : nat), n' + 0 = n').
  { induction n'. reflexivity. simpl. rewrite IHn'. reflexivity. }
  induction n, m; try reflexivity; simpl; try rewrite plus_0_r; try reflexivity.
  - rewrite IHn. simpl.
    assert (plus_m_Sn : forall (o p : nat), o + S p = S (o + p)).
    { induction o; intros; simpl; try reflexivity. rewrite IHo. reflexivity. }
    rewrite plus_m_Sn. reflexivity.
Qed.

(* by the way that add is defined trying to simplify n + 0 doesn work, look *)
Eval simpl in forall (n : nat), n + 0 = n.
(* this outputs = forall n : nat, n + 0 = n : Prop
   that + 0 is not eliminated, but the left 0 is eliminated as expected *)
Eval simpl in forall (n : nat), 0 + n = n.
(* = forall n : nat, n = n : Prop, pay atention on this >>> n = n <<<, no 0
   this is because Nat.add is defined by induction only on the firts parameter *)

Print Nat.add.
(* outputs
Nat.add = 
fix add (n m : nat) {struct n} : nat :=
  match n with (* <<------ here *)
  | 0 => m
  | S p => S (add p m)
  end
*)

(* this is another definition of add that is inductive on both arguments *)
Fixpoint addlr (a : nat) : nat -> nat :=
  fix aux (b : nat) : nat :=
    match a with
    | 0 => b
    | S a' =>
        match b with
        | 0 => S a'
        | S b' => S (S (addlr a' b'))
        end
    end.

(* then, the commutativity is much simpler to proof because of the 
   definition *)
Theorem addlr_comm' : forall (n m : nat), addlr n m = addlr m n.
  induction n, m; try reflexivity.
  simpl. rewrite IHn. reflexivity.
Qed.

(* finally here is a proof that add = addlr *)
Theorem add_addlr_eq : forall (n m : nat), Nat.add n m = addlr n m.
  induction n.
  - intros. simpl. induction m; try reflexivity.
    - intros. induction m.
      + rewrite plus_n_O. reflexivity.
      + simpl. rewrite <- plus_n_Sm. rewrite IHn. reflexivity.
Qed.