proposition: Lemma ltM_trans : forall a l l' , ltM a l l' -> forall l'', ltM a l' l'' -> ltM a l l''.
proof: Proof. induction 1. destruct 1. split. eauto with arith. intros ; rewrite H0; auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0