proposition: Theorem wf_R_lt : well_founded R_nat_lt.
proof: Proof. red; induction a; constructor; intros. { inversion H. exfalso. subst. inversion H0. } { inversion H; clear H; subst. inversion H0; clear H0; subst; auto. inversion IHa. eapply H. constructor. eapply H1. } Defined.
imports: ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Tactics.Consider ExtLib.Tactics.Injection