proposition: Lemma Zmax_le_compat : forall a b c d, a <= b -> c <= d -> Z.max a c <= Z.max b d.
proof: Proof. intros; apply Z.max_lub. apply Z.le_trans with b; auto; apply Z.le_max_l. apply Z.le_trans with d; auto; apply Z.le_max_r. Qed.
imports: ZArith List Lia