proposition: Lemma Zmin_le_compat : forall a b c d, a <= b -> c <= d -> Z.min a c <= Z.min b d.
proof: Proof. intros; apply Z.min_glb. apply Z.le_trans with a; auto; apply Z.le_min_l. apply Z.le_trans with c; auto; apply Z.le_min_r. Qed.
imports: ZArith List Lia