What is a hammer/atp within the logic of coq that does things like induction in coq?

Using Coq
1

I was curious about ATPs within the logic of Coq itself (e.g. that do induction sort of smartly). Do people know of tools better than sauto, coqhammer? (note SMTCoqhammer also uses FOL solvers/atps so I don’t think that’s quite what I’m curious about)

I had a similar discussion (that sort of ended) in Coq hammer’s gitissues: Extending hammer/sauto to use induction? · Issue #125 · lukaszcz/coqhammer · GitHub

More Context:

I wanted to use a “hammer” coq_simp_atp. to solve very simple proofs for me. e.g.

have: forall n: my_nat, O [+] n = n [+] O. by coq_simp_atp.

for example currently the above cannot be solved by by sauto. or by hammer. since they require induction e.g.

have: forall n: my_nat, O [+] n = n [+] O. induction n. by sauto. by sauto.

is the needed proof. Is there some type of hammer that does this for simple cases in coq?

Code context:

From Coq Require Import ssreflect ssrfun ssrbool.
From Hammer Require Import Tactics Hammer.

  Inductive my_nat : Type :=
    | O : my_nat
    | S : my_nat -> my_nat.

  Fixpoint add_left (n m : my_nat) : my_nat := 
    match n with
    | O => m
    | S n' => S (add_left n' m)
  end.
  Notation "x [+] y" := (add_left x y) (at level 50, left associativity).
  
  Theorem my_add_comm:
    forall n m : my_nat, n [+] m = m [+] n.
  Proof.
    intros. induction n as [| n' IH].
    - 
      have: forall n: my_nat, O [+] n = n [+] O. induction n. by sauto. by sauto.
      by sauto.
2

just saw this: Inductive proof automation