proposition: Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
proof: Proof. intros m1 m2 m3; rewrite 3 lt_slt; unfold slt; intros; eapply LO.lt_trans; eauto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia