proposition: Lemma ltM_cons : forall a l l' b n, ltM a l l' -> ltM a (cons b n l) (cons b n l').
proof: Proof. intros. unfold ltM. case H; intros. split; simpl. case (T1_eq_dec a b). auto with arith. auto. intros; case (T1_eq_dec b0 b). intro; subst b0;auto. intro;apply H1. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0