A right-recursive variant of plus: nat -> nat -> nat in Coq

right-recursive-plus-in-Coq.v

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Fixpoint plus' (n m: nat): nat := match n with | S n' => plus' n' (S m) | 0 => m end.

Lemma helper_lemma: forall n m, plus' n (S m) = S (plus' n m).
Proof.
  elim => // [n IHn m].
  by simpl; do ! rewrite IHn.
Qed.

Theorem plus_plus'_ext_eqv: forall n m, plus n m = plus' n m.
Proof.
  elim => // [n IHn m].
  by simpl; rewrite helper_lemma; rewrite IHn.
Qed.

Require Import Coq.Logic.FunctionalExtensionality.
Theorem plus_plus'_eqv: plus = plus'.
Proof.
  do 2! [apply: functional_extensionality; move => ?].
  by apply: plus_plus'_ext_eqv.
Qed.