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