proposition: Theorem wf_R_S : well_founded R_nat_S.
proof: Proof. red; induction a; constructor; intros. inversion H. inversion H; subst; auto. Defined.
imports: ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Tactics.Consider ExtLib.Tactics.Injection