proposition: Lemma max_le_regR : forall n p q, p <= q -> max p n <= max q n.
proof: Proof. intros; case (max_dec p n). intro e;rewrite e. apply le_trans with q. auto. apply le_max_l. intro e;rewrite e. apply le_max_r. Qed.
imports: Arith ArithRing Compare_dec Omega Max