proposition: Lemma lt_ltM : forall a n b l l', b < a -> ltM a l l' -> ltM a (cons b n l) l'.
proof: Proof. induction 2; split. simpl. case (T1_eq_dec a b). intro; absurd (lt a a);auto with T1. subst b;auto. auto. intros; simpl. case (T1_eq_dec b0 b). intro; subst b0; case (lt_not_gt H);auto. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0