proposition: Lemma well_founded_lt_b {B} {monoid : Monoid B} : well_founded lt_B.
proof: Proof. constructor. unfold lt_B; induction (bin_measure a); intros. - inversion H. - inversion H; subst. + constructor; eauto. + eauto. Qed.