proposition: Lemma ltM_tail : forall a n l, ltM a l (cons a n l).
proof: Proof. intros; unfold ltM. split. simpl. case (T1_eq_dec a a). intro; omega. intro; absurd (a=a);auto. intros; simpl. case (T1_eq_dec b a). intro; absurd (lt a b). subst b;auto with T1. auto. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0